A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics T₀

DOI10.1016/J.APAL.2015.04.002MaRDI QIDQ2344720zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• scientific article; zbMATH DE number 176198
• A new model for intuitionistic analysis
• A note on the interpretability logic of finitely axiomatized theories
• Intuitionistic model constructions and normalization proofs
• An interpretation of intuitionistic analysis with restricted transfinite inductive definitions
• A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
• A negationless interpretation of intuitionistic theories. II
• Implicit definability and infinitary logic in finite model theory (extended abstract)
• A negationless interpretation of intuitionistic theories
• A lower bound for intuitionistic logic

Cites work

• scientific article; zbMATH DE number 1670489 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4039890 (Why is no real title available?)
• scientific article; zbMATH DE number 3687373 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 42735 (Why is no real title available?)
• scientific article; zbMATH DE number 3494394 (Why is no real title available?)
• scientific article; zbMATH DE number 3552491 (Why is no real title available?)
• scientific article; zbMATH DE number 3556031 (Why is no real title available?)
• scientific article; zbMATH DE number 1215498 (Why is no real title available?)
• scientific article; zbMATH DE number 515742 (Why is no real title available?)
• scientific article; zbMATH DE number 1062120 (Why is no real title available?)
• scientific article; zbMATH DE number 1870423 (Why is no real title available?)
• scientific article; zbMATH DE number 1870425 (Why is no real title available?)
• scientific article; zbMATH DE number 1390277 (Why is no real title available?)
• scientific article; zbMATH DE number 1390282 (Why is no real title available?)
• scientific article; zbMATH DE number 2204757 (Why is no real title available?)
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• A well-ordering proof for Feferman's theoryT 0
• Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
• Explicit mathematics and operational set theory: some ontological comparisons
• Explicit mathematics with the monotone fixed point principle
• Explicit mathematics with the monotone fixed point principle. II: Models
• Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
• Extensional realizability
• Interpreting classical theories in constructive ones
• Kripke-Platek set theory and the anti-foundation axiom
• Monotone inductive definitions in a constructive theory of functions and classes
• Monotone inductive definitions in explicit mathematics
• On the intuitionistic strength of monotone inductive definitions
• On the proof-theoretic strength of monotone induction in explicit mathematics
• Operational set theory and small large cardinals
• Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
• Reflections on reflections in explicit mathematics
• Subsystems of second order arithmetic
• Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
• The Operational Perspective: Three Routes
• The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
• The strength of some Martin-Löf type theories
• Universes in explicit mathematics
• Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
• Wellordering proofs for metapredicative Mahlo

Cited in

(11)

• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
• Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives
• Proof theory of constructive systems: inductive types and univalence
• The operational penumbra: some ontological aspects
• Realization of analysis into Explicit Mathematics
• Research on supply chain risk assessment with intuitionistic fuzzy information
• Theories of Frege structure equivalent to Feferman's system \(\mathsf{T}_0\)
• Characterizations of ordinal analysis
• Explicit mathematics with the monotone fixed point principle
• A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2344720)