Hirst, Jeffry L.; Mummert, Carl Reverse mathematics and uniformity in proofs without excluded middle. (English) Zbl 1225.03083 Notre Dame J. Formal Logic 52, No. 2, 149-162 (2011). 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. Reviewer: Josef Berger (München) Cited in 3 ReviewsCited in 10 Documents 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 Keywords:reverse mathematics; proof theory; realizability; uniformization; intuitionistic arithmetic; subsystems of second-order arithmetic PDFBibTeX XMLCite \textit{J. L. Hirst} and \textit{C. Mummert}, Notre Dame J. Formal Logic 52, No. 2, 149--162 (2011; Zbl 1225.03083) Full Text: DOI arXiv