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

TL;DR

This paper introduces a new notion of largeness and polynomial bounds to translate proofs of certain logical sentences from a stronger to a weaker base theory, enhancing understanding of their computational complexity.

Contribution

It develops a variant of $orall ext{-largeness}$ with polynomial bounds, enabling efficient proof translation between theories using Milliken's tree theorem.

Findings

Proofs of $orall ext{-} ext{Sigma}^0_3$ sentences in $ ext{WKL}_0 + ext{RT}^2_2$ can be translated into $ ext{RCA}_0 + ext{B} ext{-} ext{Sigma}^0_2$ with polynomial size increase.

Introduces a new largeness notion and uses Milliken's tree theorem to achieve polynomial bounds.

Establishes a framework for proof translation with complexity control.

Abstract

Le Hou\'erou, 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.