Ramsey's Theorem for Pairs and Provably Recursive Functions

Notre Dame Journal of Formal Logic 50 (4):427-444 (2009)
This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In the resulting theory we show the extractability of primitive recursive programs and uniform bounds from proofs of $\forall\exists$-theorems. There are two components of this work. The first component is a general proof-theoretic result, due to the second author, that establishes conservation results for restricted principles of choice and comprehension over primitive recursive arithmetic PRA as well as a method for the extraction of primitive recursive bounds from proofs based on such principles. The second component is the main novelty of the paper: it is shown that a proof of Ramsey's theorem due to Erdős and Rado can be formalized using these restricted principles. So from the perspective of proof unwinding the computational content of concrete proofs based on $RT^2_2$ the computational complexity will, in most practical cases, not go beyond primitive recursive complexity. This even is the case when the theorem to be proved has function parameters f and the proof uses instances of $RT^2_2$ that are primitive recursive in f
Keywords Ramsey's Theorem for pairs   provably recursive functions   proof mining
Categories (categorize this paper)
DOI 10.1215/00294527-2009-019
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,727
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles
Variations on a Theme by Weiermann.Toshiyasu Arai - 1998 - Journal of Symbolic Logic 63 (3):897-925.
Accessible Recursive Functions.Stanley S. Wainer - 1999 - Bulletin of Symbolic Logic 5 (3):367-388.
Syntactic Translations and Provably Recursive Functions.Daniel Leivant - 1985 - Journal of Symbolic Logic 50 (3):682-688.
A Recursion Theoretic Analysis of the Clopen Ramsey Theorem.Peter Clote - 1984 - Journal of Symbolic Logic 49 (2):376-400.
Classifying the Provably Total Functions of Pa.Andreas Weiermann - 2006 - Bulletin of Symbolic Logic 12 (2):177-190.
Degrees of Relative Provability.Mingzhong Cai - 2012 - Notre Dame Journal of Formal Logic 53 (4):479-489.
Added to PP index

Total downloads
10 ( #444,287 of 2,197,331 )

Recent downloads (6 months)
1 ( #299,047 of 2,197,331 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature