Largeness notions and polytime translation for ∀Σ03-consequences of RT22
Published:
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^0_3\)-conservative extension of \(\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2\), where \(\forall \Sigma^0_3\) is the universal set-closure of the class of \(\Sigma^0_3\)-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^0_3\)-sentence in the theory \(\mathsf{WKL}_0 + \mathsf{RT}^2_2\) can be translated into a proof in \(\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2\) at the cost of a polynomial increase in size.
Recommended citation: Q. Le Houérou and L. Patey (2026). "Largeness notions and polytime translation for ∀Σ03-consequences of RT22."
Download Paper