关于$\mathsf{RT}^2_2$的$\forall \Sigma^0_3$推论的大性概念与多项式时间翻译

Le Houérou、Patey和Yokoyama定义了$\alpha$-大性的参数化版本，以证明$\mathsf{WKL}_0 + \mathsf{RT}^2_2$是$\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$的$\forall \Sigma^0_3$保守扩张，其中$\forall \Sigma^0_3$是$\Sigma^0_3$公式类的全称闭包。我们引入了该大性概念的一个变体，并利用基于Milliken树定理的树划分定理获得了多项式界。借助力迫解释框架，这意味着$\mathsf{WKL}_0 + \mathsf{RT}^2_2$理论中任何$\forall \Sigma^0_3$语句的证明，都可以翻译为$\mathsf{RCA}_0 + \mathsf{B}\Sigma^0_2$中的证明，且证明规模仅呈多项式增长。