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

Ramsey's theorem for n-tuples and k-colors (RT_k ⁿ) asserts that every k-coloring of [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 Π₁ ⁰ consequences, and show that RT₂ ² is Π₃ ⁰ conservative over IΣ₁ ⁰. This strengthens the proof of Chong, Slaman and Yang that RT² ₂ does not imply IΣ₂ ⁰, and shows that RT₂ ² 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 Π₃ ⁰-conservation theorems.