Formalizing forcing arguments in subsystems of second-order arithmetic (Q2563983)

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.