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.002zbMATH Open1371.03093OpenAlexW648945431MaRDI QIDQ2344720FDOQ2344720
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
Recommendations
- scientific article
- 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
interpretabilityextensional realizabilityFeferman's explicit mathematicsmaking a detour via intuitionistic theoriestree representation of sets
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)
Cites Work
- Subsystems of second order arithmetic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interpreting classical theories in constructive ones
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The strength of some Martin-Löf type theories
- Title not available (Why is that?)
- Constructive Zermelo-Fraenkel set theory and the limited principle of omniscience
- Title not available (Why is that?)
- Title not available (Why is that?)
- Explicit mathematics with the monotone fixed point principle. II: Models
- 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
- Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
- Explicit mathematics and operational set theory: some ontological comparisons
- A well-ordering proof for Feferman's theoryT 0
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- Title not available (Why is that?)
- Universes in explicit mathematics
- Extending the system T\(_0\) of explicit mathematics: The limit and Mahlo axioms
- Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
- On the proof-theoretic strength of monotone induction in explicit mathematics
- Title not available (Why is that?)
- Kripke-Platek set theory and the anti-foundation axiom
- The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
- Monotone inductive definitions in a constructive theory of functions and classes
- Explicit mathematics with the monotone fixed point principle
- Title not available (Why is that?)
- Monotone inductive definitions in explicit mathematics
- Title not available (Why is that?)
- Extensional realizability
- On the intuitionistic strength of monotone inductive definitions
- Wellordering proofs for metapredicative Mahlo
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Operational Perspective: Three Routes
Cited In (11)
- 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
- 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\)
- A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
- Characterizations of ordinal analysis
- Explicit mathematics with the monotone fixed point principle
- Proof Theory of Constructive Systems: Inductive Types and Univalence
- A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).
- The Operational Penumbra: Some Ontological Aspects
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)
