Ramsey's theorem for pairs and provably recursive functions (Q987936)

The paper under review adresses the strength of \textit{F. P. Ramsey}'s theorem for pairs [Proc. Lond. Math. Soc. (2) 30, 264--286 (1929; JFM 55.0032.04)] over a weak base theory applying methods of `proof mining'. The authors work in a weak base theory \({\mathcal T}\), based on fragments E-G\(_n\)A\(^\omega\) of extensional arithmetic in the language of functionals of all finite types, introduced by the second author [Arch. Math. Logic 36, No.~1, 31--71 (1996; Zbl 0882.03050)]. Thus, \({\mathcal T}\) is obtained by considering the union E-G\(_\infty\)A\(^\omega\) of these systems and adding QF-AC (quantifier-free axiom of choice from functions to numbers and from numbers to functions) as well as WKL (weak König's Lemma). For \(n\geq 1\), let RT\(_n^2\) denote Ramsey's theorem for \(n\)-colorings of \([{\mathbb N}]^2\) and, given an \(n\)-coloring \(c:[{\mathbb N}]^2\to \{0,1,\ldots,n-1\}\), let RT\(_n^2(c)\) be the statement expressing the fact that Ramsey's theorem holds for \(c\). The main technical result of the paper establishes that over \({\mathcal T}\) one can prove RT\(_n^2(c)\) from a suitable instance \(\Pi_0^1\text{-CA}(\tilde{\varphi}(c))\) of \(\Pi_0^1\)-comprehension. The authors obtain this result by a logical analysis of the proof of Ramsey's theorem for pairs due to Erdős and Rado. Combining this with previous results of \textit{U. Kohlenbach} [Ann. Pure Appl. Logic 95, No. 1--3, 257--285 (1998; Zbl 0945.03088)] on the arithmetical content of restricted forms of comprehension and choice, the authors obtain the second main result of the paper: If \[ {\mathcal T}\vdash \forall f\in{\mathbb N}^{\mathbb N} (\Pi_0^1\text{-CA}(\varphi(f))\wedge \forall k\in{\mathbb N} (\text{RT}_2^2(\psi(f,k)))\to \exists n\in{\mathbb N} A_{qf}(f,n)), \] where \(\varphi\), \(\psi\) are closed terms of \({\mathcal T}\) of suitable types, then there exists a primitive recursive (in the sense of Kleene) functional \(\Phi\) such that \[ \widehat{\text{E-PA}}^\omega\!\!\!\upharpoonright \,\,\vdash \,\, \forall f\in{\mathbb N}^{\mathbb N} A_{qf}(f,\Phi(f)). \] Moreover, the proof-theoretic method provides an extraction algorithm for \(\Phi\) from a given proof.