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

Abstract

We construct an ${\ll }^2$-solution (also known as a weakly low solution) to ${\mathrm{D}}^2$ within $\mathrm{B}{\Sigma }_3^0$ and prove the ${\ll }^2$-basis theorem for ${\mathrm{RT}}^2$ over $\mathrm{B}{\Sigma }_3^0$. 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{WK}{\mathsf{L}}_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}{\Sigma }_2^0$. 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.