Formalizing forcing arguments in subsystems of second-order arithmetic

DOI10.1016/0168-0072(96)00003-6MaRDI QIDQ2563983zbMATH OpenOpenAlexFDO

Authors Jeremy Avigad

Publication date 26 January 1997

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

Full work available at URL https://doi.org/10.1016/0168-0072(96)00003-6

zbMATH Keywords

conservation theoremmodel-theoretic forcing

Mathematics Subject Classification ID

Model-theoretic forcing (03C25) Second- and higher-order arithmetic and fragments (03F35)

Review text

The main theorem of the paper is a sharpening of the conservation theorem of Harrington and Brown-Simpson. It is proved that \(\text{WKL}^+_0\) is conservative over \(\text{RCA}_0\), i.e., that one can translate \(\text{WKL}^+_0\) proofs to \(\text{RCA}_0\) proofs without a significant increase in size. This is done by showing that certain model-theoretic forcing argument can be formalized in the base theory.

Recommendations

• Harrington's conservation theorem redone
• A variant of Mathias forcing that preserves \(\mathsf{ACA}_0\)
• Some conservation results on weak König's lemma
• On some formalized conservation results in arithmetic

Cites work

• Fragments of arithmetic
• Herbrand analyses
• scientific article; zbMATH DE number 440479 (Why is no real title available?)
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 4004177 (Why is no real title available?)
• On the strength of König's duality theorem for countable bipartite graphs
• Recursively enumerable sets and degrees
• Subsystems of second order arithmetic
• The Baire category theorem in weak subsystems of second-order arithmetic
• ∏ 0 1 Classes and Degrees of Theories

Cited in

(25)

• On some formalized conservation results in arithmetic
• A new conservation result of \(\text{WKL}_0\) over \(\text{RCA}_0\)
• The proof-theoretic strength of Ramsey's theorem for pairs and two colors
• Some conservation results on weak König's lemma
• Saturated models of universal theories
• A variant of Mathias forcing that preserves \(\mathsf{ACA}_0\)
• A new model construction by making a detour via intuitionistic theories. III: Ultrafinitistic proofs of conservations of \(\Sigma_1^1\) collection
• Unifying the model theory of first-order and second-order arithmetic via \(\mathrm{WKL}_0^\ast\)
• Strict \({\varPi^1_1}\)-reflection in bounded arithmetic
• On the strength of Ramsey's theorem for pairs
• Interpreting weak König's lemma using the arithmetized completeness theorem
• Formalizing non-standard arguments in second-order arithmetic
• Proof theory in philosophy of mathematics
• On ^1_1 conservativity for ^1_2 theories in second order arithmetic
• 10th Asian Logic Conference
• Subsets coded in elementary end extensions
• A Model-Theoretic Approach to Ordinal Analysis
• Forcing in Proof Theory
• A marriage of Brouwer's intuitionism and Hilbert's finitism. I: Arithmetic
• A complexity analysis of functional interpretations
• On mathematical instrumentalism
• Marginalia on a theorem of Woodin
• A new model construction by making a detour via intuitionistic theories. IV: A closer connection between \(\mathrm{KP} \omega\) and \(\mathrm{BI}\).
• An isomorphism theorem for models of weak König's lemma without primitive recursion
• Harrington's conservation theorem redone

This page was built for publication: Formalizing forcing arguments in subsystems of second-order arithmetic

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