Formalizing forcing arguments in subsystems of second-order arithmetic (Q2563983)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 961101
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Formalizing forcing arguments in subsystems of second-order arithmetic |
scientific article; zbMATH DE number 961101 |
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
0.8177263140678406
0 references
0.8009572625160217
0 references
0.7982344031333923
0 references
0.7844682931900024
0 references
