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

Ramsey's theorem for n-tuples and k-colors (RTkn) asserts that every k-coloring of [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 Pi(0)(1) consequences, and show that RT22 is Pi(0)(3) conservative over I Sigma(0)(1). This strengthens the proof of Chong, Slaman and Yang that RT22 does not imply I Sigma(0)(2), and shows that RT22 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 Pi(0)(3)-conservation theorems. (C) 2018 Elsevier Inc. All rights reserved.