English

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

Logic 2026-02-26 v2

Abstract

Le Hou\'erou, Patey and Yokoyama defined a parameterized version of α\alpha-largeness to prove that WKL0+RT22\mathsf{WKL}_0 + \mathsf{RT}^2_2 is a Σ30\forall \Sigma^0_3-conservative extension of RCA0+BΣ20\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2, where Σ30\forall \Sigma^0_3 is the universal set-closure of the class of Σ30\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 Σ30\forall \Sigma^0_3-sentence in the theory WKL0+RT22\mathsf{WKL}_0 + \mathsf{RT}^2_2 can be translated into a proof in RCA0+BΣ20\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2 at the cost of a polynomial increase in size.

Keywords

Cite

@article{arxiv.2602.11906,
  title  = {Largeness notions and polytime translation for $\forall \Sigma^0_3$-consequences of $\mathsf{RT}^2_2$},
  author = {Quentin Le Houérou and Ludovic Patey},
  journal= {arXiv preprint arXiv:2602.11906},
  year   = {2026}
}

Comments

32 pages