[FOM] Primitive Recursive Pigeons

[Stephen G Simpson]

A.P. Hazen writes:
 >     About three years ago, I remember hearing that someone had shown 
 > that the PIGEON-HOLE PRINCIPLE, over some  very basic theory, yielded 
 > primitive recursion (and so was a sufficient supplement to the very 
 > basic theory to bring it up to the power of PRA).  Does someone have 
 > references? or details?   [...]

Dear Allen,

I think this result or something like it is due to Takeshi Yamazaki.
I seem to remember that I posted something on FOM about this.  I can't
find the posting, but here is an e-mail that I sent to Jeffry Hirst
around that time.

Best regards,
-- Steve

-----

  From: Stephen G Simpson <simpson at math.psu.edu>
  To: jlh at math.appstate.edu
  Cc: yamazaki at math.psu.edu
  Subject: RT(1) results
  Date: Mon, 16 Oct 2000 15:49:34 -0400 (EDT)

  Dear Jeff,

  Let RT(1) be Ramsey's theorem for exponent 1, i.e., (forall n)RT(1,n),
  i.e., the pigeonhole principle, i.e., for all n, if f:N --> {1,...,n}
  then there is an infinite homogeneous set.

  In your thesis, you proved that RT(1) is equivalent to Pi^0_1
  bounding, over RCA_0.

  Let RCA_0^* be as in the Simpson/Smith paper, and in the last section
  of SOSOA, i.e., RCA_0 minus Sigma^0_1 induction, plus exponentiation,
  plus Sigma^0_0 induction,

  Yamazaki just pointed out that RT(1) implies Sigma^0_1-IND over
  RCA_0^*.  The proof goes like this.  Assume RT(1).  We will prove
  bounded Sigma^0_1 comprehension.  Given b and a Sigma^0_1 formula
  (exists y)theta(x,y).  Define f:N --> 2^b by putting f(z)=(e_x:x<b)
  where e_x=1 if (exists y<z)theta(x,y), e_x=0 otherwise.  Let Z be an
  infinite homogeneous set for f.  Then for all z in Z and x<b we have
  (exists y)theta(x,y) if and only if (exists y<z)theta(x,y).  This
  proves the result.

  Combining this with your result, we have the following improvement of
  your result: RT(1) is equivalent to Pi^0_1 bounding, over RCA_0^*.

  A consequence of this is that RT(3) is equivalent to arithmetical
  comprehension over RCA_0^*.

  It still seems to be open whether RT(3,2) is equivalent to
  arithmetical comprehension over RCA_0^*.

  Yamazaki can show that RT(2) implies Sigma^0_1-IND, over a system of
  2nd order bounded arithmetic (without exponentiation).

  Best regards,
  -- Steve