Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms

DOI10.1016/S0168-0072(01)00076-8zbMath1002.03052OpenAlexW2015181892WikidataQ114656179 ScholiaQ114656179MaRDI QIDQ5957853

Gerhard Jäger, Thomas Studer

Publication date: 7 January 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(01)00076-8

zbMATH Keywords

proof theoryexplicit mathematicslimit axiomMahlo axiomnonmonotone inductive definitionsrecursive inaccessibilityreflection principles

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15) Inductive definability (03D70)

Related Items

Decidability for some justification logics with negative introspection, A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting), Universes in explicit mathematics, Explicit mathematics: power types and overloading, EXPLICIT MATHEMATICS AND OPERATIONAL SET THEORY: SOME ONTOLOGICAL COMPARISONS, Proof Theory of Constructive Systems: Inductive Types and Univalence, Full operational set theory with unbounded existential quantification and power set, Reflections on reflections in explicit mathematics, A NOTE ON THEORIES FOR QUASI-INDUCTIVE DEFINITIONS, 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, Universes over Frege structures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-theoretic analysis of KPM
• Constructivism in mathematics. An introduction. Volume I
• Well-ordering proofs for Martin-Löf type theory
• Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
• The strength of some Martin-Löf type theories
• Extending Martin-Löf type theory by one Mahlo-universe
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo
• A well-ordering proof for Feferman's theoryT 0
• Universes in explicit mathematics