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.