FOM: logical status of pigeonhole principles, part 1

[Stephen G Simpson]

Matthew Frank 3 Dec 2000 writes:

 > Robert Tragesser asked various questions about Erdos's probabilistic
 > method.
 > > (4) What is the reverse mathematics of "the Pigeonhole Principle?"
 > 
 > Since you ask...we formalize this as:
 > for every n,
 > for every function f: [1,n+1]->[1,n]
 > there exist distinct a,b less than n+2 with f(a)=f(b)
 > 
 > The following proof by induction on n contains only bounded quantifiers,
 > and so stays within the base theory RCA_0.
 > ...

Here Matt Frank is referring to one particular finitary form of the
pigeonhole principle: if you put n+1 pigeons into n pigeonholes, some
pigeonhole will receive at least 2 pigeons.  Call this PHP(n+1,n,2).
The Erdos notation for this is n+1->(2)^1_n.

Another finitary form of the pigeonhole principle is PHP(2n,n,2) or,
in the Erdos notation, 2n->(n)^1_2: if you put 2n pigeons into n
pigeonholes, some pigeonhole will receive at least 2 pigeons.

Surprisingly, the logical status of "for all n, PHP(n+1,n,2)" is
different from that of "for all n, PHP(2n,n,2)"!  The second is known
to be provable in I Delta_0 + Omega_1 (this is due to Alan Woods I
think) but the first is not.

This distinction plays a large role in a currently interesting and
exciting area of f.o.m. research: What theorems of elementary number
theory and combinatorics are provable in what systems of bounded
arithmetic?  Here ``bounded arithmetic'' refers to any of a number of
formal systems for first order arithmetic without exponentiation.  One
of these systems is I Delta_0 + Omega_1.  See for instance
Hayek/Pudlak, "Metamathematics of First-Order Arithmetic",
Springer-Verlag, 1993.  A number of interesting papers have been
published in recent years.  Some of the authors are Macintyre,
D'Aquino, Berarducci, Intriglia.  Recently I heard Angus Macintyre
give a good talk on this subject, at the Schmerl 60th Birthday
Symposium.

In my view, the foundational aims of the above-mentioned research area
(number theory in bounded arithmetic) are broadly similar to those of
Reverse Mathematics [at a different level of course, because in my
book on Reverse Mathematics (Subsystems of Second Order Arithmetic,
Springer-Verlag, 1999, http://www.math.psu.edu/simpson/sosoa/), all of
the formal systems are in the language of second order arithmetic and
assume full exponentiation].

However, for reasons that are not well understood, Macintyre has
openly exhibited great hostility to Reverse Mathematics.  See also my
FOM posting "sour grapes vis a vis Reverse Mathematics", FOM, 1 March
1998, referring to Macintyre's essay "The Strength of Weak Systems",
which was published as part of the proceedings of a symposium on
Wittgenstein, Kluwer Academic Publishers, 1986, pages 43-59.

Can someone help explain Macintyre's point of view?

Another logical aspect of the pigeonhole principle is that, for each
particular n, statements such as PHP(n+1,n,2) and PHP(2n,n,2) are
formalizable as particular sentences A_n, B_n, ... of propositional
calculus, and a lot of work has been done to find upper and lower
bounds on the length and complexity of proofs of such sentences in
various propositional proof systems.  A reference for this subject is
Krajicek's book "Bounded Arithmetic, Propositional Logic, and
Complexity Theory", Cambridge University Press, 1995.  Alasdair
Urquhart mentioned this aspect in his recent FOM posting.

-- Steve