A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of _1¹ collection

DOI10.1016/J.APAL.2022.103207MaRDI QIDQ2111109zbMATH OpenOpenAlexWikidataFDO

Authors Kentaro Sato

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

zbMATH Keywords

interpretationrealizabilityintuitionistic forcing\(\Pi_2^1\) conservation\(\Sigma_1^ 1\)-DC\(\Sigma_1^1\) collection

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25) Constructive and recursive analysis (03F60)

Recommendations

• On some formalized conservation results in arithmetic
• A Conservation Result Concerning Bounded Theories and the Collection Axiom
• A proof-theoretic analysis of collection
• Harrington's conservation theorem redone
• Conservativity of ultrafilters over subsystems of second order arithmetic

Cites work

• scientific article; zbMATH DE number 5838313 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 3342822 (Why is no real title available?)
• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• A note on predicative ordinal analysis. I. Iterated comprehension and transfinite induction
• A well-ordering proof for Feferman's theoryT 0
• Bounded inductive dichotomy: separation of open and clopen determinacies with finite alternatives in constructive contexts
• Double helix in large large cardinals and iteration of elementary embeddings
• Elementary inductive dichotomy: separation of open and clopen determinacies with infinite alternatives
• Factorization of polynomials and \(\Sigma ^ 0_ 1\) induction
• Forcing for hat inductive definitions in arithmetic
• Forcing under Anti‐Foundation Axiom: An expression of the stalks
• Formalizing forcing arguments in subsystems of second-order arithmetic
• From hierarchies to well-foundedness
• Full and hat inductive definitions are equivalent in NBG
• Interpreting classical theories in constructive ones
• Lifschitz' realizability
• On the relation between choice and comprehension principles in second order arithmetic
• Relative predicativity and dependent recursion in second-order set theory and higher-order theories
• Truncation and semi-decidability notions in applicative theories

Cited in

(2)

• A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
• 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. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection

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