Reverse mathematics and uniformity in proofs without excluded middle

DOI10.1215/00294527-1306163zbMATH Open1225.03083arXiv1010.5165OpenAlexW2089230867WikidataQ57951149 ScholiaQ57951149MaRDI QIDQ540402FDOQ540402

Authors: Jeffry L. Hirst, Carl Mummert 

Publication date: 3 June 2011

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Abstract: 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 $P{i}_2^1$ sentence of a certain form is provable using E-HA${}^{o}mega$ 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 extit{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.

Full work available at URL: https://arxiv.org/abs/1010.5165

Recommendations

• Classical provability of uniform versions and intuitionistic provability
• Reverse mathematics, trichotomy and dichotomy
• Classical consequences of continuous choice principles from intuitionistic analysis
• scientific article; zbMATH DE number 2247263
• scientific article; zbMATH DE number 3924748

zbMATH Keywords

proof theoryrealizabilityreverse mathematicsuniformizationintuitionistic arithmeticsubsystems of second-order arithmetic

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Constructive and recursive analysis (03F60)

Cited In (14)

• Reverse mathematics and completeness theorems for intuitionistic logic
• Classical provability of uniform versions and intuitionistic provability
• Using Ramsey's theorem once
• Reverse mathematics and Weihrauch analysis motivated by finite complexity theory
• Intuitionistic Provability versus Uniform Provability in $$\mathsf{RCA}$$
• On robust theorems due to Bolzano, Weierstrass, Jordan, and Cantor
• ON WEIHRAUCH REDUCIBILITY AND INTUITIONISTIC REVERSE MATHEMATICS
• Automata, Languages and Programming
• Weihrauch and constructive reducibility between existence statements
• On the strength of marriage theorems and uniformity
• Classical consequences of continuous choice principles from intuitionistic analysis
• Parallelizations in Weihrauch reducibility and constructive reverse mathematics
• Pincherle's theorem in reverse mathematics and computability theory
• On avoidability of formulas with reversal

This page was built for publication: Reverse mathematics and uniformity in proofs without excluded middle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q540402)