大规模性概念与多项式翻译对于RT^2_2的∀Σ^0_3后果
Largeness notions and polytime translation for $\forall Σ^0_3$-consequences of $\mathsf{RT}^2_2$
AI总结：
本文提出了一种大规模性概念的变体，并利用树分割定理和forcing解释框架，证明了WKL_0 + RT^2_2理论中∀Σ^0_3句子的证明可转换为RCA_0 + BΣ^0_2中的证明，且规模增加为多项式级。
摘要：
Le Houérou、Patey和Yokoyama定义了一个参数化的α-大规模性概念，以证明WKL_0 + RT^2_2是RCA_0 + BΣ^0_2的∀Σ^0_3保守扩展，其中∀Σ^0_3是Σ^0_3公式的闭包集。我们引入了这一大规模性概念的一个变体，并利用基于Milliken树定理的树分割定理获得了多项式界限。借助forcing解释框架，这使得任何在WKL_0 + RT^2_2理论中证明的∀Σ^0_3句子都可以转换为RCA_0 + BΣ^0_2中的证明，仅需以多项式增长的规模为代价。
英文摘要：
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 + \mathsf{RT}^2_2$ can be translated into a proof in $\mathsf{RCA}_0 + \mathsf{B}Σ^0_2$ at the cost of a polynomial increase in size.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
