The Journal of Symbolic Logic

Research Article

On the strength of Ramsey's theorem for pairs

Peter A. Cholaka1, Carl G. Jockuscha2 and Theodore A. Slamana3

a1 Department of Mathematics, University of Notre Dame, Notre Dame, IN 46556-5683, USA, E-mail: Peter.Cholak.l@nd.edu

a2 Department of Mathematics, University of Illinois, at Urbana-Champaign, 1409 W. Green Street, Urbana, Illinois 61801-2975, USA, E-mail: jockusch@math.uiuc.edu

a3 Department of Mathematics, University of California, Berkeley, CA 94720-3840, USA, E-mail: slaman@math.berkeley.edu

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 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

  • Ramsey's Theorem;
  • conservation;
  • reverse mathematics;
  • recursion theory;
  • computability theory