Term extraction and Ramsey's theorem for pairs

Journal of Symbolic Logic 77 (3):853-895 (2012)
  Copy   BIBTEX


In this paper we study with proof-theoretic methods the function(al) s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functional provably recursive from $RCA_0 + COH + \Pi _1^0 - CP$ are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that $WKL_0 + \Pi _1^0 - CP + COH$ is $\Pi _1^0 $ -conservative over PRA. Recent work of the first author showed that $\Pi _1^0 + CP + COH$ is equivalent to a weak variant of the Bolzano-Weierstraß principle. This makes it possible to use our results to analyze not only combinatorial but also analytical proofs. For Ramsey's theorem for pairs and two colors $\left( {RT_2^2 } \right)$ we obtain the upper bounded that the type 2 functionals provable recursive relative to $RCA_0 + \sum\nolimits_2^0 {IA + RT_2^2 } $ are in T₁. This is the fragment of Gödel's system T containing only type 1 recursion—roughly speaking it consists of functions of Ackermann type. With this we also obtain a uniform method for the extraction of T₁-bounds from proofs that use RT2..... Moreover, this yields a new proof of the fact that $WKL_0 + \sum\nolimits_2^0 {IA} + RT_2^2 $ is $\Pi _1^0 $ -conservative over $RCA_0 + \sum\nolimits_2^0 { - IA} $ . The results are obtained in two steps: in the first step a term including Skolem functions for the above principles is extracted from a given proof. This is done using Gödel's functional interpretation. After this the term is normalized, such that only specific instances of the Skolem functions are used. In the second step this term is interpreted using $\Pi _1^0 $ -comprehension. The comprehension is then eliminated in favor of induction using either elimination of monotone Skolem functions (for COH) or Howard's ordinal analysis of bar recursion (for $RT_2^2 $



    Upload a copy of this work     Papers currently archived: 76,264

External links

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

Through your library

Similar books and articles

Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Stable Ramsey's Theorem and Measure.Damir D. Dzhafarov - 2011 - Notre Dame Journal of Formal Logic 52 (1):95-112.
On the Ramsey property for sets of reals.Ilias G. Kastanas - 1983 - Journal of Symbolic Logic 48 (4):1035-1045.
Ramsey’s representation theorem.Richard Bradley - 2004 - Dialectica 58 (4):483–497.
On theoretical constructs and Ramsey constants.R. M. Martin - 1966 - Philosophy of Science 33 (1/2):1-13.
An ordinal partition avoiding pentagrams.Jean A. Larson - 2000 - Journal of Symbolic Logic 65 (3):969-978.
A new proof that analytic sets are Ramsey.Erik Ellentuck - 1974 - Journal of Symbolic Logic 39 (1):163-165.
Nonstandard combinatorics.Joram Hirshfeld - 1988 - Studia Logica 47 (3):221 - 232.
A recursion theoretic analysis of the clopen Ramsey theorem.Peter Clote - 1984 - Journal of Symbolic Logic 49 (2):376-400.
On the Indecomposability of $\omega^{n}$.Jared R. Corduan & François G. Dorais - 2012 - Notre Dame Journal of Formal Logic 53 (3):373-395.


Added to PP

20 (#565,488)

6 months
1 (#449,844)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Primitive Recursion and the Chain Antichain Principle.Alexander P. Kreuzer - 2012 - Notre Dame Journal of Formal Logic 53 (2):245-265.
Program extraction for 2-random reals.Alexander P. Kreuzer - 2013 - Archive for Mathematical Logic 52 (5-6):659-666.
From Bolzano-Weierstraß to Arzelà-Ascoli.Alexander P. Kreuzer - 2014 - Mathematical Logic Quarterly 60 (3):177-183.

Add more citations

References found in this work

On the Strength of Ramsey's Theorem.David Seetapun & Theodore A. Slaman - 1995 - Notre Dame Journal of Formal Logic 36 (4):570-582.
A cohesive set which is not high.Carl Jockusch & Frank Stephan - 1993 - Mathematical Logic Quarterly 39 (1):515-530.
Reverse mathematics: the playground of logic.Richard A. Shore - 2010 - Bulletin of Symbolic Logic 16 (3):378-402.

View all 16 references / Add more references