Reflections on reflections in explicit mathematics

DOI10.1016/J.APAL.2005.05.008zbMath1094.03048OpenAlexW1981436950MaRDI QIDQ2566068

Gerhard Jäger, Thomas Strahm

Publication date: 22 September 2005

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

Full work available at URL: https://doi.org/10.1016/j.apal.2005.05.008

zbMATH Keywords

surveyexplicit mathematicsreflection principles2-universe axiom

Mathematics Subject Classification ID

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

Related Items (6)

A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP ⋮ On Feferman's operational set theory \textsf{OST} ⋮ EXPLICIT MATHEMATICS AND OPERATIONAL SET THEORY: SOME ONTOLOGICAL COMPARISONS ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ A flexible type system for the small Veblen ordinal ⋮ A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Ein Wohlordnungsbeweis für das Ordinalzahlensystem T(J). (A proof of the wellordering of the ordinal number system T(J))
• Constructivism in mathematics. An introduction. Volume II
• The proof-theoretic analysis of \(\Sigma_{1}^{1}\) transfinite dependent choice
• 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
• Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo
• The strength of admissibility without foundation
• The proof-theoretic analysis of transfinitely iterated fixed point theories
• Wellordering proofs for metapredicative Mahlo
• A well-ordering proof for Feferman's theoryT 0
• Universes in explicit mathematics
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms

This page was built for publication: Reflections on reflections in explicit mathematics