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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,410

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

On some formalized conservation results in arithmetic.P. Clote, P. Hájek & J. Paris - 1990 - Archive for Mathematical Logic 30 (4):201-218.
Weak König's Lemma Implies Brouwer's Fan Theorem: A Direct Proof.Hajime Ishihara - 2006 - Notre Dame Journal of Formal Logic 47 (2):249-252.
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.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Complex analysis in subsystems of second order arithmetic.Keita Yokoyama - 2007 - Archive for Mathematical Logic 46 (1):15-35.
A feasible theory for analysis.Fernando Ferreira - 1994 - Journal of Symbolic Logic 59 (3):1001-1011.
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.
Measure theory and weak König's lemma.Xiaokang Yu & Stephen G. Simpson - 1990 - Archive for Mathematical Logic 30 (3):171-180.
Reverse mathematics and a Ramsey-type König's Lemma.Stephen Flood - 2012 - Journal of Symbolic Logic 77 (4):1272-1280.
Hindman's theorem: An ultrafilter argument in second order arithmetic.Henry Towsner - 2011 - Journal of Symbolic Logic 76 (1):353 - 360.
About the proof-theoretic ordinals of weak fixed point theories.Gerhard Jäger & Barbara Primo - 1992 - Journal of Symbolic Logic 57 (3):1108-1119.
Sequent calculus proof theory of intuitionistic apartness and order relations.Sara Negri - 1999 - Archive for Mathematical Logic 38 (8):521-547.
Which set existence axioms are needed to prove the cauchy/peano theorem for ordinary differential equations?Stephen G. Simpson - 1984 - Journal of Symbolic Logic 49 (3):783-802.

Analytics

Added to PP
2013-11-23

Downloads
28 (#574,026)

6 months
8 (#372,793)

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 - 1975 - 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