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

Foundations of classical theories (including reverse mathematics) (03B30) Axiomatics of classical set theory and its fragments (03E30) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Other aspects of forcing and Boolean-valued models (03E40) Relative consistency and interpretations (03F25)

Cites Work

Unnamed Item
Unnamed Item
Unnamed Item
Unnamed Item
Unnamed Item
Unnamed Item
Unnamed Item
Unnamed Item
Classes and truths in set theory
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
The strength of extensionality. II: Weak weak set theories without infinity
The strength of extensionality. I: Weak weak set theories with infinity
Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
Proof-theoretic investigations on Kruskal's theorem
Fixed points in Peano arithmetic with ordinals
A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
Full and hat inductive definitions are equivalent in NBG
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\)
Formalizing forcing arguments in subsystems of second-order arithmetic
A few more dissimilarities between second-order arithmetic and set theory
Interpreting classical theories in constructive ones
Forcing for hat inductive definitions in arithmetic
RELATIVE PREDICATIVITY AND DEPENDENT RECURSION IN SECOND-ORDER SET THEORY AND HIGHER-ORDER THEORIES
The proof-theoretic analysis of transfinitely iterated quasi least fixed points
The strength of admissibility without foundation
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
TRUTHS, INDUCTIVE DEFINITIONS, AND KRIPKE-PLATEK SYSTEMS OVER SET THEORY
PROOF-THEORETIC STRENGTHS OF WEAK THEORIES FOR POSITIVE INDUCTIVE DEFINITIONS
A new method for establishing conservativity of classical systems over their intuitionistic version
A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
Open determinacy for class games
Forcing under Anti‐Foundation Axiom: An expression of the stalks
A survey of proof theory
On the relationship between ATR₀ and
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}\).