On the strength of Ramsey's theorem for pairs

Abstract We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RT k n denote Ramsey's theorem for k –colorings of n –element sets, and let RT <∞ n denote (∀ k )RT k n . Our main result on computability is: For any n ≥ 2 and any computable (recursive) k –coloring of the n –element sets of natural numbers, there is an infinite homogeneous set X with X ″ ≤ T 0 ( n ) . Let I Σ n and B Σ n denote the Σ n induction and bounding schemes, respectively. Adapting the case n = 2 of the above result (where X is low 2 ) to models of arithmetic enables us to show that RCA 0 + I Σ 2 + RT 2 2 is conservative over RCA 0 + I Σ 2 for Π 1 1 statements and that RCA 0 + I Σ 3 + RT <∞ 2 is Π 1 1 -conservative over RCA 0 + I Σ 3 . It follows that RCA 0 + RT 2 2 does not imply B Σ 3 . In contrast, J. Hirst showed that RCA 0 + RT <∞ 2 does imply B Σ 3 , and we include a proof of a slightly strengthened version of this result. It follows that RT <∞ 2 is strictly stronger than RT 2 2 over RCA 0 .