Wellordering proofs for metapredicative Mahlo

DOI10.2178/JSL/1190150043zbMath1032.03050OpenAlexW2096744225MaRDI QIDQ4532614

Thomas Strahm

Publication date: 17 March 2004

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://boris.unibe.ch/115328/1/S0022481200009981.pdf

zbMATH Keywords

proof-theoretic strengthexplicit mathematicsproof-theoretic ordinalmetapredicativity

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50)

Related Items (5)

The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice ⋮ On the relationship between fixed points and iteration in admissible set theory without foundation ⋮ Reflections on reflections in explicit mathematics ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\) ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

Cites Work

• Unnamed Item
• Proof-theoretic analysis of KPM
• Constructivism in mathematics. An introduction. Volume I
• Fixed point theories and dependent choice
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• The strength of Martin-Löf type theory with a superuniverse. I
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• The strength of admissibility without foundation
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• Universes in explicit mathematics
• The strength of Martin-Löf type theory with a superuniverse. II

This page was built for publication: Wellordering proofs for metapredicative Mahlo