Harrington's conservation theorem redone (Q948908)

The theorem in the title states that the second-order arithmetic \(\text{WKL}_0\) is \(\Pi^1_1\)-conservative over the theory \(\text{RCA}_0\). Harrington proved this model-theoretically, previously. Now, the authors give a proof-theoretic proof. Their set-up is sequent calculus, and they replace Weak König's Lemma (in \(\text{WKL}_0)\) by its contrapositive, \(\text{FAN}_0\), formulated as a rule. Given a (formal) poof of a \(\Pi^1_1\)-formula \(XF(X)\), they use the method of cut elimination so that in the resulting proof of \(F(X)\) only \(\Sigma^0_1\)-formulas occur (certainly no second-order quantifier). The authors' crucial observation is that a bounded formula can be regulated, and so this new proof is normalized further. This step requires case analysis of each rule, but shows that the \(\text{FAN}_0\)-rule is not necessary. In the last section, the authors make observations on contrast between classical and intuitionistic systems. For instance, the conservation theorem of the above type does not hold intuitionistically. On the other hand, the theory \(\text{RCA}_0^-+\text{FAN}\) is inconsistent classically, but intuitionistically it is \(\Pi^0_2\)-conservative over PRA.