A new model construction by making a detour via intuitionistic theories. IV: A closer connection between KP and BI.

DOI10.1016/J.APAL.2024.103422MaRDI QIDQ6539428FDOQ6539428

Authors: Kentaro Sato 

Publication date: 14 May 2024

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

interpretabilityrealizabilitytree representation of sets\(\Pi_{2}^ {1}\) conservationKripke-style forcinglinearity of admissibles

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Other aspects of forcing and Boolean-valued models (03E40) 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)

Cites Work

• Title not available (Why is that?)
• Classes and truths in set theory
• Interpreting classical theories in constructive ones
• Title not available (Why is that?)
• A new method for establishing conservativity of classical systems over their intuitionistic version
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proof-theoretic investigations on Kruskal's theorem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Zur Beweistheorie Der Kripke-Platek-Mengenlehre Über Den Natürlichen Zahlen
• The consistency of classical set theory relative to a set theory with intu1tionistic logic
• A survey of proof theory
• Formalizing forcing arguments in subsystems of second-order arithmetic
• Title not available (Why is that?)
• Relative predicativity and dependent recursion in second-order set theory and higher-order theories
• Forcing under Anti‐Foundation Axiom: An expression of the stalks
• The strength of extensionality. II: Weak weak set theories without infinity
• The strength of extensionality. I: Weak weak set theories with infinity
• Fixed points in Peano arithmetic with ordinals
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• From hierarchies to well-foundedness
• On the relationship between ATR₀ and
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Title not available (Why is that?)
• Proof-theoretic strengths of weak theories for positive inductive definitions
• The strength of admissibility without foundation
• Full and hat inductive definitions are equivalent in NBG
• Truths, inductive definitions, and Kripke-Platek systems over set theory
• 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
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• Forcing for hat inductive definitions in arithmetic
• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• The proof-theoretic analysis of transfinitely iterated quasi least fixed points
• Open determinacy for class games
• A few more dissimilarities between second-order arithmetic and set theory
• Admissible extensions of subtheories of second order arithmetic

This page was built for publication: A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).

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