Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Quentin Le Houérou, Ludovic Patey

TL;DR

This work advances the reverse-mathematics analysis of RT^2_2 by introducing a refined, polynomially tractable notion of α-largeness, denoted α-largeness$^*( heta)$, and proving that RT^2_2 admits polynomial bounds with respect to this notion. It develops a robust combinatorial framework based on a finite Milliken-tree theorem and a forcing interpretation to transfer proofs from WKL_0 + RT^2_2 to RCA_0 + BΣ^0_2 without exponential blowup. The main contributions are (i) a polynomial bound for RT^2_2 in terms of α-largeness$^*( heta)$, (ii) an explicit forcing-based translation showing that any ∀Σ^0_3-sentence provable in WKL_0 + RT^2_2 has a polynomial-size proof in RCA_0 + BΣ^0_2, and (iii) a detailed analysis of the interaction between largeness, sparsity, and tree-partition combinatorics to support these translations. The results yield a significant speedup improvement over prior exponential bounds and deepen the understanding of conservativity phenomena in the presence of RT^2_2.

Abstract

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.

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

TL;DR

This work advances the reverse-mathematics analysis of RT^2_2 by introducing a refined, polynomially tractable notion of α-largeness, denoted α-largeness, and proving that RT^2_2 admits polynomial bounds with respect to this notion. It develops a robust combinatorial framework based on a finite Milliken-tree theorem and a forcing interpretation to transfer proofs from WKL_0 + RT^2_2 to RCA_0 + BΣ^0_2 without exponential blowup. The main contributions are (i) a polynomial bound for RT^2_2 in terms of α-largeness, (ii) an explicit forcing-based translation showing that any ∀Σ^0_3-sentence provable in WKL_0 + RT^2_2 has a polynomial-size proof in RCA_0 + BΣ^0_2, and (iii) a detailed analysis of the interaction between largeness, sparsity, and tree-partition combinatorics to support these translations. The results yield a significant speedup improvement over prior exponential bounds and deepen the understanding of conservativity phenomena in the presence of RT^2_2.

Abstract

Le Houérou, Patey and Yokoyama defined a parameterized version of -largeness to prove that is a -conservative extension of , where is the universal set-closure of the class of -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 -sentence in the theory can be translated into a proof in at the cost of a polynomial increase in size.
Paper Structure (18 sections, 43 theorems, 13 equations, 2 figures)

This paper contains 18 sections, 43 theorems, 13 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Notation
  3. Notions of largeness
  4. Largeness and sparsity
  5. $\alpha$-largeness
  6. $\alpha$-largeness$(\theta)$
  7. $\alpha$-largeness${}^*(\theta)$
  8. Combinatorics of largeness${}^*(\theta)$
  9. Construction and deconstruction
  10. Relation to largeness$(\theta)$
  11. Cut
  12. Sparsity
  13. Pigeonhole principle
  14. Partition theorem for regular trees
  15. Grouping principle
  16. ...and 3 more sections

Key Result

Theorem 2.6

Let $k \geq 2$. If $F \subseteq_{\mathtt{fin}} \mathbb{N}$ is $\bbomega^{k+4}$-large, then it is $\mathsf{RT}^2_k$-$\bbomega$-large.

Figures (2)

  • Figure 1: Upper bounds of $\mathsf{P}$-$\bbomega^n$-largeness for various notions of largeness and various $\mathsf{RT}$-like statements, under the assumptions of $g$-sparsity for some primitive recursive function $g$ and of sufficiently large minimum.
  • Figure 2: Polynomial simulations between the various theories in \ref{['sec:translation']}.

Theorems & Definitions (88)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Theorem 2.6: Ketonen and Solovay ketonen1981rapidly
  • Theorem 2.7: Kołodziejczyk and Yokoyama kolo2020some
  • Theorem 2.8: Kołodziejczyk and Yokoyama kolo2020some
  • Lemma 2.9: Kołodziejczyk and Yokoyama kolo2020some
  • Theorem 2.10: Le Houérou and Patey houerou2026partition
  • ...and 78 more