Journal of Symbolic Logic 56 (3):964 - 973 (1991)

Jaap Van Oosten
Leiden University
F. Richman raised the question of whether the following principle of second order arithmetic is valid in intuitionistic higher order arithmetic 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 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.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275064
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 53,645
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Topos Theory.P. T. Johnstone - 1982 - Journal of Symbolic Logic 47 (2):448-450.

Add more references

Citations of this work BETA

Basic Subtoposes of the Effective Topos.Sori Lee & Jaap van Oosten - 2013 - Annals of Pure and Applied Logic 164 (9):866-883.

Add more citations

Similar books and articles

A Small Reflection Principle for Bounded Arithmetic.Rineke Verbrugge & Albert Visser - 1994 - Journal of Symbolic Logic 59 (3):785-812.
In What Sense is Kantian Principle of Contradiction Non-Classical?Srećko Kovač - 2008 - Logic and Logical Philosophy 17 (3):251-274.
A General Notion of Realizability.Lars Birkedal - 2002 - Bulletin of Symbolic Logic 8 (2):266-282.
Two Remarks on the Lifschitz Realizability Topos.Jaap van Oosten - 1996 - Journal of Symbolic Logic 61 (1):70-79.
A Realizability Interpretation for Classical Arithmetic.Jeremy Avigad - 2002 - Bulletin of Symbolic Logic 8 (3):439-440.
Lifschitz' Realizability.Jaap van Oosten - 1990 - Journal of Symbolic Logic 55 (2):805-821.


Added to PP index

Total views
6 ( #1,041,741 of 2,349,062 )

Recent downloads (6 months)
1 ( #512,311 of 2,349,062 )

How can I increase my downloads?


My notes