Notre Dame Journal of Formal Logic 52 (2):149-162 (2011)

We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $\Pi^1_2$ sentence of a certain form is provable using E-HA ${}^\omega$ along with the axiom of choice and an independence of premise principle, the sequential form of the statement is provable in the classical system RCA. We obtain this and similar results using applications of modified realizability and the Dialectica interpretation. These results allow us to use techniques of classical reverse mathematics to demonstrate the unprovability of several mathematical principles in subsystems of constructive analysis
Keywords reverse mathematics   proof theory   Dialectica   realizability   uniformization
Categories (categorize this paper)
Reprint years 2011
DOI 10.1215/00294527-1306163
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: 71,489
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

Realizability.A. S. Troelstra - 2000 - Bulletin of Symbolic Logic 6 (4):470-471.
Countable Functionals.S. C. Kleene - 1962 - Journal of Symbolic Logic 27 (3):359-360.
Filters on Computable Posets.Steffen Lempp & Carl Mummert - 2006 - Notre Dame Journal of Formal Logic 47 (4):479-485.
A Note on Goodman's Theorem.Ulrich Kohlenbach - 1999 - Studia Logica 63 (1):1-5.

Add more references

Citations of this work BETA

Pincherle's Theorem in Reverse Mathematics and Computability Theory.Dag Normann & Sam Sanders - 2020 - Annals of Pure and Applied Logic 171 (5):102788.
Using Ramsey’s theorem once.Jeffry L. Hirst & Carl Mummert - 2019 - Archive for Mathematical Logic 58 (7-8):857-866.
On Weihrauch Reducibility and Intuitionistic Reverse Mathematics.Rutger Kuyper - 2017 - Journal of Symbolic Logic 82 (4):1438-1458.

View all 6 citations / Add more citations

Similar books and articles

Questioning Constructive Reverse Mathematics.I. Loeb - 2012 - Constructivist Foundations 7 (2):131-140.
Intuitionistic Mathematics and Wittgenstein.Wenceslao J. Gonzalez - 1991 - History and Philosophy of Logic 12 (2):167-183.
On the Indecomposability of $\omega^{N}$.Jared R. Corduan & François G. Dorais - 2012 - Notre Dame Journal of Formal Logic 53 (3):373-395.
Perfect Validity, Entailment and Paraconsistency.Neil Tennant - 1984 - Studia Logica 43 (1-2):181 - 200.
Reverse Mathematics: The Playground of Logic.Richard A. Shore - 2010 - Bulletin of Symbolic Logic 16 (3):378-402.
Reverse Mathematics and Π21 Comprehension.Carl Mummert & Stephen G. Simpson - 2005 - Bulletin of Symbolic Logic 11 (4):526-533.


Added to PP index

Total views
30 ( #383,731 of 2,520,891 )

Recent downloads (6 months)
1 ( #405,457 of 2,520,891 )

How can I increase my downloads?


My notes