Reverse Mathematics and Uniformity in Proofs without Excluded Middle

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


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



    Upload a copy of this work     Papers currently archived: 92,100

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

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

40 (#399,415)

6 months
6 (#526,006)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

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 7 citations / Add more citations

References found in this work

Interpretation of analysis by means of constructive functionals of finite types.Georg Kreisel - 1959 - In A. Heyting (ed.), Constructivity in mathematics. Amsterdam,: North-Holland Pub. Co.. pp. 101--128.
Countable functionals.S. C. Kleene - 1959 - Journal of Symbolic Logic 27 (3):81--100.
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.

View all 6 references / Add more references