1 results
Extension of Lifschitz' realizability to higher order arithmetic,and a solution to a problem of F. Richman
-
- Journal:
- The Journal of Symbolic Logic / Volume 56 / Issue 3 / September 1991
- Published online by Cambridge University Press:
- 12 March 2014, pp. 964-973
- Print publication:
- September 1991
-
- Article
- Export citation
-
F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic HAH:
and if not, whether assuming Church's Thesis CT and Markov's Principle MP would help. Blass and Scedrov gave models of 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 HAH + CT + MP + ECT0, 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.
