Formalizing forcing arguments in subsystems of second-order arithmetic (Q2563983): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/0168-0072(96)00003-6 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2085905338 / rank | |||
Normal rank | |||
Revision as of 15:23, 19 March 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Formalizing forcing arguments in subsystems of second-order arithmetic |
scientific article |
Statements
Formalizing forcing arguments in subsystems of second-order arithmetic (English)
0 references
26 January 1997
0 references
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.
0 references
conservation theorem
0 references
model-theoretic forcing
0 references
