Reflections on reflections in explicit mathematics

DOI10.1016/j.apal.2005.05.008zbMath1094.03048MaRDI 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

survey; explicit mathematics; reflection principles; 2-universe axiom

Mathematics Subject Classification ID

03E70: Nonclassical and second-order set theories

03F35: Second- and higher-order arithmetic and fragments

03F50: Metamathematics of constructive systems

03F15: Recursive ordinals and ordinal notations

Related Items

On Feferman's operational set theory \textsf{OST}

Cites Work

• 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
• 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