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

TL;DR

This paper introduces a new low basis theorem for Ramsey's theorem for pairs within weak systems of arithmetic, using Mathias forcing, simplifying proofs of known conservativity results.

Contribution

It constructs a weakly low solution to D^2 within BΣ^0_3 and proves a new basis theorem for RT^2, extending the understanding of computability in weak arithmetic systems.

Findings

Constructed an $ ilde{ ext{l}}^2$-solution within BΣ^0_3.

Proved the $ ilde{ ext{l}}^2$-basis theorem for RT^2 and related principles.

Provided simpler proofs of $ ext{Pi}^1_1$-conservativity results.

Abstract

We construct an $\ll^2$-solution (also known as a weakly low solution) to ${\mathrm{D}^2}$ within ${\mathrm{B}\Sigma^0_{3}}$ and prove the $\ll^2$-basis theorem for $\mathrm{RT}^2$ over ${\mathrm{B}\Sigma^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 $\omega$-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\H{o}s-Moser principle, within $\mathrm{I}\Sigma^0_{2}$. These results provide simpler proofs of known results on the $\Pi^1_1$-conservativities of $\mathrm{RT}^2, \mathrm{RT}^2_2$ and $\mathrm{EM}_{<\infty}$ as corollaries.