The proof-theoretic strength of Ramsey's theorem for pairs and two colors

Abstract

Ramsey's theorem for $n$-tuples and $k$-colors ($\mathsf{RT}^n_k$) asserts that every k-coloring of $[\mathbb{N}]^n$ admits an infinite monochromatic subset. We study the proof-theoretic strength of Ramsey's theorem for pairs and two colors, namely, the set of its $Π^0_1$ consequences, and show that $\mathsf{RT}^2_2$ is $Π^0_3$ conservative over $\mathsf{I}Σ^0_1$. This strengthens the proof of Chong, Slaman and Yang that $\mathsf{RT}^2_2$ does not imply $\mathsf{I}Σ^0_2$, and shows that $\mathsf{RT}^2_2$ is finitistically reducible, in the sense of Simpson's partial realization of Hilbert's Program. Moreover, we develop general tools to simplify the proofs of $Π^0_3$-conservation theorems.