Largeness notions and polytime translation for $\forall {\Sigma }_3^0$-consequences of ${\mathsf{RT}}_2^2$

Abstract

Le Houérou, Patey and Yokoyama defined a parameterized version of $\alpha$-largeness to prove that ${\mathsf{WKL}}_0+{\mathsf{RT}}_2^2$ is a $\forall {\Sigma }_3^0$-conservative extension of ${\mathsf{RCA}}_0+\mathsf{B}{\Sigma }_2^0$, where $\forall {\Sigma }_3^0$ is the universal set-closure of the class of ${\Sigma }_3^0$-formulas. We introduce a variant of this notion of largeness and obtain polynomial bounds, using a tree partition theorem based on Milliken's tree theorem. Thanks to the framework of forcing interpretation, this yields that any proof of a $\forall {\Sigma }_3^0$-sentence in the theory ${\mathsf{WKL}}_0+{\mathsf{RT}}_2^2$ can be translated into a proof in ${\mathsf{RCA}}_0+\mathsf{B}{\Sigma }_2^0$ at the cost of a polynomial increase in size.

32 pages