Harrington’s conservation theorem redone

&
Archive for Mathematical Logic 47 (2):91-100 (2008)
  Copy   BIBTEX

Abstract

Leo Harrington showed that the second-order theory of arithmetic WKL 0 is ${\Pi^1_1}$ -conservative over the theory RCA 0. Harrington’s proof is model-theoretic, making use of a forcing argument. A purely proof-theoretic 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.

Categories

Keywords

Reprint years

DOI

10.1007/s00153-008-0080-8

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 107,099

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Formalizing forcing arguments in subsystems of second-order arithmetic.Jeremy Avigad - 1996 - Annals of Pure and Applied Logic 82 (2):165-191.
On some formalized conservation results in arithmetic.P. Clote, P. Hájek & J. Paris - 1990 - Archive for Mathematical Logic 30 (4):201-218.
Reflection ranks via infinitary derivations.James Walsh - forthcoming - Archive for Mathematical Logic:1-17.
An Effective Conservation Result for Nonstandard Arithmetic.Erik Palmgren - 2000 - Mathematical Logic Quarterly 46 (1):17-24.
On Formalization of Model-Theoretic Proofs of Gödel's Theorems.Makoto Kikuchi & Kazuyuki Tanaka - 1994 - Notre Dame Journal of Formal Logic 35 (3):403-412.
The Jordan curve theorem and the Schönflies theorem in weak second-order arithmetic.Nobuyuki Sakamoto & Keita Yokoyama - 2007 - Archive for Mathematical Logic 46 (5-6):465-480.
Cut-elimination in second order logic.O. Serebriannikov - 1988 - Bulletin of the Section of Logic 17 (3-4):159-160.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
About the proof-theoretic ordinals of weak fixed point theories.Gerhard Jäger & Barbara Primo - 1992 - Journal of Symbolic Logic 57 (3):1108-1119.
On uniform weak König's lemma.Ulrich Kohlenbach - 2002 - Annals of Pure and Applied Logic 114 (1-3):103-116.

Analytics

Added to PP
2013-11-23

Downloads
38 (#692,627)

6 months
3 (#1,291,302)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Add more citations

References found in this work

Proof theory.Gaisi Takeuti - 1987 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Subsystems of Second Order Arithmetic.Stephen G. Simpson - 1999 - Studia Logica 77 (1):129-129.
Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Fragments of arithmetic.Wilfried Sieg - 1985 - Annals of Pure and Applied Logic 28 (1):33-71.

View all 15 references / Add more references