a1 Department of Mathematics, University of Notre Dame, Notre Dame, IN 46556-5683, USA, E-mail: [email protected]
a2 Department of Mathematics, University of Illinois, at Urbana-Champaign, 1409 W. Green Street, Urbana, Illinois 61801-2975, USA, E-mail: [email protected]
a3 Department of Mathematics, University of California, Berkeley, CA 94720-3840, USA, E-mail: [email protected]
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 low2) to models of arithmetic enables us to show that RCA0 + IΣ2 + RT2 2 is conservative over RCA0 + IΣ2 for Π1 1 statements and that RCA0 + IΣ3 + RT<∞ 2 is Π1 1-conservative over RCA0 + IΣ3. It follows that RCA0 + RT2 2 does not imply BΣ3. In contrast, J. Hirst showed that RCA0 + 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 RT2 2 over RCA 0.
(Received October 07 1998)
(Revised April 13 1999)
Key words and phrases