×

Reverse mathematics and uniformity in proofs without excluded middle. (English) Zbl 1225.03083

The paper studies the relationship between systems of intuitionistic arithmetic in all finite types and subsystems of classical second-order arithmetic. It shows that when certain statements are provable in subsystems of the former, using intuitionistic predicate calculus, related sequential statements are provable in weak subsystems of the latter.

MSC:

03F50 Metamathematics of constructive systems
03B30 Foundations of classical theories (including reverse mathematics)
03F35 Second- and higher-order arithmetic and fragments
03F60 Constructive and recursive analysis
PDFBibTeX XMLCite
Full Text: DOI arXiv