We prove that RCA₀ + RT $RT\begin{array}{*{20}{c}} 2 \\ 2 \\ \end{array} $ ̸͢ WKL₀ by showing that for any set C not of PA-degree and any set A, there exists an infinite subset G of A or ̅Α, such that G ⊕ C is also not of PA-degree.

We show that, for every partition F of the pairs of natural numbers and for every set C, if C is not recursive in F then there is an infinite set H, such that H is homogeneous for F and C is not recursive in H. We conclude that the formal statement of Ramsey's Theorem for Pairs is not strong enough to prove , the comprehension scheme for arithmetical formulas, within the base theory , the comprehension scheme for recursive formulas. (...) We also show that Ramsey's Theorem for Pairs is strong enough to prove some sentences in first order arithmetic which are not provable within . In particular, Ramsey's Theorem for Pairs is not conservative over for -sentences. (shrink)

We study the proof-theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RT n k denote Ramsey's theorem for k-colorings of n-element sets, and let RT $^n_{ denote (∀ k)RT n k . 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\Sigma_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. (shrink)