Ramsey's theorem for pairs, collection, and proof size

Abstract

We prove that any proof of a $\forall {\Sigma }_2^0$ sentence in the theory ${\mathrm{WKL}}_0+{\mathrm{RT}}_2^2$ can be translated into a proof in ${\mathrm{RCA}}_0$ at the cost of a polynomial increase in size. In fact, the proof in ${\mathrm{RCA}}_0$ can be found by a polynomial-time algorithm. On the other hand, ${\mathrm{RT}}_2^2$ has non-elementary speedup over the weaker base theory ${\mathrm{RCA}}_0^{\ast }$ for proofs of ${\Sigma }_1$ sentences. We also show that for $n\ge 0$, proofs of ${\Pi }_{n+2}$ sentences in $\mathrm{B}{\Sigma }_{n+1}+\exp$ can be translated into proofs in $\mathrm{I}{\Sigma }_n+\exp$ at polynomial cost. Moreover, the ${\Pi }_{n+2}$-conservativity of $\mathrm{B}{\Sigma }_{n+1}+\exp$ over $\mathrm{I}{\Sigma }_n+\exp$ can be proved in $\mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n\ge 1$, this answers a question of Clote, Hájek, and Paris.

33 pages. Corrected definition of forcing in Section 4, with appropriate modifications to the argument. Minor editorial changes throughout the text