On the quantifier of limiting realizability

N. A. Shanin

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VII, Tome 60 (1976), pp. 209-220

Résumé

In the searches for “contentwise”-interesting constructive analogs of the theorems of classiaal mathematics, there occur useful logical connectives occupying an intermediate position between $\underset{\cdot}\exists$ and $\exists$ and between $\underset{\cdot}\vee$ and $\vee$ [$\underset{\cdot}\exists xF$ denotes $\rceil\forall x\rceil F$, and $(F_1\underset{\cdot}\vee F_2)$ denotes $\rceil(\rceil F_1\&\rceil F_2)$]. Two logical connectives of this types, suggested by the theory of limitedly computable (semicomputable) functions and defined in terms of the basic logical connectives of constructive logic, viz., the quantifier $\underset{\to}\exists$ of limiting realizability and the quantifier $\underset{\to}\vee$ oflimiting disjunction, are introduced into consideration in the article. A number of properties are established for these logical connectives.