Extension of Lifschitz' Realizability to Higher Order Arithmetic, and a Solution to a Problem of F. Richman
van Oosten, Jaap
J. Symbolic Logic, Tome 56 (1991) no. 1, p. 964-973 / Harvested from Project Euclid
F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic $\mathbf{HAH}$: $\forall X\lbrack\forall x(x \in X \vee \neg x \in X) \wedge \forall Y(\forall x(x \in Y \vee \neg x \in Y) \rightarrow \forall x(x \in X \rightarrow x \in Y) \vee \forall x \neg(x \in X \wedge x \in Y)) \rightarrow \exists n\forall x(x \in X \rightarrow x = n)\rbrack$, and if not, whether assuming Church's Thesis CT and Markov's Principle MP would help. Blass and Scedrov gave models of $\mathbf{HAH}$ in which this principle, which we call RP, is not valid, but their models do not satisfy either CT or MP. In this paper a realizability topos Lif is constructed in which CT and MP hold, but RP is false. (It is shown, however, that $RP$ is derivable in $\mathbf{HAH} + \mathrm{CT} + \mathrm{MP} + \mathrm{ECT}_0$, so RP holds in the effective topos.) Lif is a generalization of a realizability notion invented by V. Lifschitz. Furthermore, Lif is a subtopos of the effective topos.
Publié le : 1991-09-15
Classification:  $|mathbf{HAH}$,  realizability,  tripos,  topos,  03F50,  03G30
@article{1183743743,
     author = {van Oosten, Jaap},
     title = {Extension of Lifschitz' Realizability to Higher Order Arithmetic, and a Solution to a Problem of F. Richman},
     journal = {J. Symbolic Logic},
     volume = {56},
     number = {1},
     year = {1991},
     pages = { 964-973},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183743743}
}
van Oosten, Jaap. Extension of Lifschitz' Realizability to Higher Order Arithmetic, and a Solution to a Problem of F. Richman. J. Symbolic Logic, Tome 56 (1991) no. 1, pp.  964-973. http://gdmltest.u-ga.fr/item/1183743743/