On the proof-theoretic strength of monotone induction in explicit mathematics

DOI10.1016/S0168-0072(96)00040-1zbMath0877.03027OpenAlexW2005199052MaRDI QIDQ1356976

Michael Rathjen, Andreas Schlüter, Thomas Glaß

Publication date: 4 November 1997

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(96)00040-1

zbMATH Keywords

stabilityProof theoryexplicit mathematicsadmissible setsmonotone inductionasymmetric interpretation

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Computability and recursion theory on ordinals, admissible sets, etc. (03D60) Relative consistency and interpretations (03F25) Inductive definability (03D70)

Related Items

On the intuitionistic strength of monotone inductive definitions ⋮ Intuitionistic fixed point logic ⋮ The Operational Perspective: Three Routes ⋮ Explicit mathematics: power types and overloading ⋮ The Operational Penumbra: Some Ontological Aspects ⋮ Proof Theory of Constructive Systems: Inductive Types and Univalence ⋮ Explicit mathematics with the monotone fixed point principle ⋮ 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\)

Cites Work

• Generalized recursion theory. Proceedings of the 1972 Oslo symposium
• Ein Wohlordnungsbeweis für das Ordinalzahlensystem T(J). (A proof of the wellordering of the ordinal number system T(J))
• Monotone inductive definitions in a constructive theory of functions and classes
• Logic colloquium '78. Proceedings of the colloquium held in Mons, August 1978.
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Algebra and logic. Papers from the 1974 Summer Research Institute of the Australian Mathematical Society, Monash University, Australia
• The strength of some Martin-Löf type theories
• Understanding uniformity in Feferman's explicit mathematics
• On monotone vs. nonmonotone induction
• A well-ordering proof for Feferman's theoryT 0
• Monotone inductive definitions in explicit mathematics
• 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