{"id":"arxiv/2602.11906","url":"https://arxiv.org/abs/2602.11906","tags":["math.LO"],"score":0,"title":"Largeness notions and polytime translation for $\\forall Σ^0_3$-consequences of $\\mathsf{RT}^2_2$","domain":"math.LO","source":"arxiv","authors":["Quentin Le Houérou","Ludovic Patey"],"reviews":0,"subject":"math.LO","summary":"Le Houérou, Patey and Yokoyama defined a parameterized version of $α$-largeness to prove that $\\mathsf{WKL}_0 + \\mathsf{RT}^2_2$ is a $\\forall Σ^0_3$-conservative extension of $\\mathsf{RCA}_0 + \\mathsf{B}Σ^0_2$, where $\\forall Σ^0_3$ is the universal set-closure of the class of $Σ^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 Σ^0_3$-sentence in the theory $\\mathsf{WKL}_0 +…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-02-12","reactions":{}}