Realization of analysis into Explicit Mathematics

DOI10.2307/2694980zbMath0993.03075OpenAlexW2120826243MaRDI QIDQ4328839

Sergei Tupailo

Publication date: 25 September 2002

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

Full work available at URL: https://doi.org/10.2307/2694980

zbMATH Keywords

explicit mathematicsinterpretationsecond-order arithmetic

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)

Related Items (3)

A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ Characterizing the interpretation of set theory in Martin-Löf type theory ⋮ Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe

Cites Work

• Well-ordering proofs for Martin-Löf type theory
• Inaccessibility in constructive set theory and type theory
• The strength of some Martin-Löf type theories
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. II
• A well-ordering proof for Feferman's theoryT 0

This page was built for publication: Realization of analysis into Explicit Mathematics