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

Leszek Aleksander Kołodziejczyk, Tin Lok Wong, Keita Yokoyama

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 polynomia…