Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

DOI10.1016/S0168-0072(02)00065-9zbMath1022.03045MaRDI QIDQ1861330

Sergei Tupailo

Publication date: 16 March 2003

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

zbMATH Keywords

lower boundrealizabilityconstructive set theoryexplicit mathematicsfoundations of constructive mathematicsMahlo principlesMartin-Löf's type theoriesset representative

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)

Related Items (9)

On the intuitionistic strength of monotone inductive definitions ⋮ A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ 2003 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquim '03 ⋮ Characterizing the interpretation of set theory in Martin-Löf type theory ⋮ Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms ⋮ Reflections on reflections in explicit mathematics ⋮ On the Strength of the Uniform Fixed Point Principle in Intuitionistic 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof-theoretic analysis of KPM
• Ordinal notations based on a weakly Mahlo cardinal
• Well-ordering proofs for Martin-Löf type theory
• Inaccessibility in constructive set theory and type theory
• Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM
• Proof theory of reflection
• The strength of some Martin-Löf type theories
• Realizing Mahlo set theory in type theory
• 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
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo
• Constructive set theory
• Realization of analysis into Explicit Mathematics
• Wellordering proofs for metapredicative Mahlo
• A well-ordering proof for Feferman's theoryT 0
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms

This page was built for publication: Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe