Harrington's conservation theorem redone

Leo Harrington showed that the second-order theory of arithmetic WKL0 is 1 1-conservative over the theory RCA0. Harrington's proof is model-theoretic, making use of a forcing argument. A purely prooftheoretic proof, avoiding forcing, has been eluding the efforts of researchers. In this short paper, we present a proof of Harrington's result using a cut-elimination argument.

• Type: Journal
• Year: 2008
• Where: AML
• Authors: Fernando Ferreira, Gilda Ferreira
• Keywords: AML 2008, Leo Harrington, Second-order Theory, Theory Rca0