A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
DOI10.1016/J.APAL.2022.103207OpenAlexW4307726500WikidataQ115221864 ScholiaQ115221864MaRDI QIDQ2111109
Publication date: 23 December 2022
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.2022.103207
realizabilityinterpretationintuitionistic forcing\(\Pi_2^1\) conservation\(\Sigma_1^ 1\)-DC\(\Sigma_1^1\) collection
Constructive and recursive analysis (03F60) Foundations of classical theories (including reverse mathematics) (03B30) Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
- Double helix in large large cardinals and iteration of elementary embeddings
- Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
- Bounded inductive dichotomy: separation of open and clopen determinacies with finite alternatives in constructive contexts
- 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
- 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
- Lifschitz' realizability
- On the relation between choice and comprehension principles in second order arithmetic
- A NOTE ON PREDICATIVE ORDINAL ANALYSIS I: ITERATED COMPREHENSION AND TRANSFINITE INDUCTION
- TRUNCATION AND SEMI-DECIDABILITY NOTIONS IN APPLICATIVE THEORIES
- A well-ordering proof for Feferman's theoryT 0
- A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC
- Forcing under Anti‐Foundation Axiom: An expression of the stalks
This page was built for publication: A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
