Universes in explicit mathematics

DOI10.1016/S0168-0072(00)00057-9zbMath0980.03061OpenAlexW1973691337MaRDI QIDQ5939842

Thomas Studer, Gerhard Jäger, Reinhard Kahle

Publication date: 12 March 2002

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(00)00057-9

zbMATH Keywords

proof-theoretic strengthsystems of explicit mathematics with universes

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (9)

Wellordering proofs for metapredicative Mahlo ⋮ Formal Universes ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ 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\) ⋮ Universes over Frege structures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Constructivism in mathematics. An introduction. Volume I
• The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
• Well-ordering proofs for Martin-Löf type theory
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• The strength of Martin-Löf type theory with a superuniverse. I
• N-strictness in applicative theories
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• The strength of admissibility without foundation
• A fine hierarchy of partition cardinals
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• Uniform inseparability in explicit mathematics
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms

This page was built for publication: Universes in explicit mathematics