Abstract:
The Pigeon Hole Principle (PHP) asserts that if m > n then it is impossible
to put m pigeons into n holes in such a way that each hole contains
at most
one pigeon. This principle is ubiquitous in its applications to elementary
number theory, finite combinatorics and finite algebra. Most mathematicians
would regard it as self evident, but only very weak forms appear among
the
``usual'' axioms. So in an axiomatic development of mathematics it
must
be proved somehow, and a very natural question to ask is how strong
the
assumptions need to be (in, say, axiom systems for bounded arithmetic)
in
order to be able to prove various forms of PHP?
Similarly, by the completeness theorem for propositional calculus,
tautologies expressing PHP for fixed choices of m,n must be theorems
of
propositional calculus. These tautologies are short - of size polynomially
bounded in m,n. The question is, how large must their proofs be, especially
if the ``complexity'' (e.g., depth) of the formulas appearing is
restricted?
In particular, PHP is a source of candidates for tautologies which
naive
automatic theorem proving schemes may find hard.
These questions turn out to be related, and considerable progress has
been
made during the past twenty five years. Part of this, including some
very
recent work, will be surveyed, with particular emphasis on Weak Pigeon
Hole
Principles - the case where m is significantly larger than n.
I will argue that in spite of all the progress, many of the most important
questions remain open.