A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)

DOI10.1016/j.apal.2015.04.002zbMath1371.03093OpenAlexW648945431MaRDI QIDQ2344720

Kentaro Sato

Publication date: 15 May 2015

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.2015.04.002

zbMATH Keywords

interpretabilityextensional realizabilityFeferman's explicit mathematicsmaking a detour via intuitionistic theoriestree representation of sets

Mathematics Subject Classification ID

Axiomatics of classical set theory and its fragments (03E30) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Combinatory logic and lambda calculus (03B40) Relative consistency and interpretations (03F25)

Related Items

A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC, Characterizations of ordinal analysis, Research on supply chain risk assessment with intuitionistic fuzzy information, Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives, The Operational Penumbra: Some Ontological Aspects, Proof Theory of Constructive Systems: Inductive Types and Univalence, A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection

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
• Unnamed Item
• Unnamed Item
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
• Operational set theory and small large cardinals
• Monotone inductive definitions in a constructive theory of functions and classes
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
• The strength of some Martin-Löf type theories
• On the proof-theoretic strength of monotone induction in explicit mathematics
• Extensional realizability
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• Reflections on reflections in explicit mathematics
• Interpreting classical theories in constructive ones
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• Kripke-Platek Set Theory and the Anti-Foundation Axiom
• EXPLICIT MATHEMATICS AND OPERATIONAL SET THEORY: SOME ONTOLOGICAL COMPARISONS
• The Operational Perspective: Three Routes
• Explicit mathematics with the monotone fixed point principle
• Explicit mathematics with the monotone fixed point principle. II: Models
• Wellordering proofs for metapredicative Mahlo
• A well-ordering proof for Feferman's theoryT 0
• Monotone inductive definitions in explicit mathematics
• On the intuitionistic strength of monotone inductive definitions
• Universes in explicit mathematics
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms