Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Low-like basis theorems for Ramsey's theorem for pairs in first-order arithmetic

Hiroyuki Ikari, Keita Yokoyama

TL;DR

This work investigates the first-order strength of Ramsey-type theorems for pairs by constructing low-like ($ll^2$) solutions to their natural decompositions, including $\mathrm{COH}$, $\mathrm{D}^2_2$, $\mathrm{D}^2$, and $\mathrm{sEM}_{<\infty}$. The authors develop $ll^2$-basis theorems using Mathias forcing inside effectively coded $\omega$-models of $\mathsf{WKL_0}$, working within $\mathrm{I}\Sigma^0_{2}$ and $\mathrm{B}\Sigma^0_3$ to obtain low-like solutions and, in turn, $\Pi^1_1$-conservativity results for the Ramsey principles. Key contributions include $ll^2$-basis theorems for $\mathrm{COH}$, $\mathrm{EM}_{<\infty}$, and $\mathrm{D}^2$, as well as a new presentation showing that $\mathrm{RT}^2$ (and its variants) yield simpler conservation proofs and potential polynomial-time proof transformations. The work thus clarifies the first-order consequences of Ramsey-type theorems and provides a unified forcing-based approach to obtaining low-like bases under weak induction, with implications for proof theory and reverse mathematics.

Abstract

We construct an $\ll^2$-solution (also known as a weakly low solution) to ${\mathrm{D}^2}$ within ${\mathrm{B}Σ^0_{3}}$ and prove the $\ll^2$-basis theorem for $\mathrm{RT}^2$ over ${\mathrm{B}Σ^0_{3}}$. The $\ll^2$-basis theorem is a variant of the low basis theorem, which has recently received focus in the context of the first-order part of Ramsey type theorems. For the construction, we use Mathias forcing in an effectively coded $ω$-model of $\mathsf{WKL_0}$ to ensure sufficient computability under the system with weaker induction. Using a similar method, we also show the $\ll^2$-basis theorem for $\mathrm{RT}^2_2$ and $\mathrm{EM}_{<\infty}$, a version of Erdős-Moser principle, within $\mathrm{I}Σ^0_{2}$. These results provide simpler proofs of known results on the $Π^1_1$-conservativities of $\mathrm{RT}^2, \mathrm{RT}^2_2$ and $\mathrm{EM}_{<\infty}$ as corollaries.

Low-like basis theorems for Ramsey's theorem for pairs in first-order arithmetic

TL;DR

This work investigates the first-order strength of Ramsey-type theorems for pairs by constructing low-like () solutions to their natural decompositions, including , , , and . The authors develop -basis theorems using Mathias forcing inside effectively coded -models of , working within and to obtain low-like solutions and, in turn, -conservativity results for the Ramsey principles. Key contributions include -basis theorems for , , and , as well as a new presentation showing that (and its variants) yield simpler conservation proofs and potential polynomial-time proof transformations. The work thus clarifies the first-order consequences of Ramsey-type theorems and provides a unified forcing-based approach to obtaining low-like bases under weak induction, with implications for proof theory and reverse mathematics.

Abstract

We construct an -solution (also known as a weakly low solution) to within and prove the -basis theorem for over . The -basis theorem is a variant of the low basis theorem, which has recently received focus in the context of the first-order part of Ramsey type theorems. For the construction, we use Mathias forcing in an effectively coded -model of to ensure sufficient computability under the system with weaker induction. Using a similar method, we also show the -basis theorem for and , a version of Erdős-Moser principle, within . These results provide simpler proofs of known results on the -conservativities of and as corollaries.
Paper Structure (10 sections, 17 theorems, 16 equations)

This paper contains 10 sections, 17 theorems, 16 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Formalized computability
  4. Ramsey's theorem
  5. The $\ll^n$-relation and low-like basis theorems
  6. Low-like basis theorems for the splits of Ramsey's theorem
  7. The $\ll^2$-basis theorem for $\mathrm{COH}$
  8. The $\ll^2$-basis theorem for Erdős-Moser principle
  9. The $\ll^2$-basis theorem for $\mathrm{D}^2_{2}$ and $\mathrm{D}^2_{}$
  10. Conclusions

Key Result

Theorem 2.6

Let $n,m\ge 1$. Then $\mathsf{RCA_0}$ proves the following.

Theorems & Definitions (50)

  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Definition 2.4: Turing jump
  • Definition 2.5: Low sets
  • Theorem 2.6
  • Theorem 2.7: Low basis theorem HaPu
  • Theorem 2.8: Primitive recursion sosoa
  • Remark 2.9
  • Theorem 2.10
  • ...and 40 more