We formulate the pigeonhole principle as follows. Consider the case that there are $n$ pigeons and $n-1$ holes. Let $x_{i,j}$ be the Boolean variable denoting that $\text{pigeon}_i$ sits in $\text{hole}_j$, where $1\le i\le n,\,1\le j\le n-1$. (Note that we introduce indices here only to succinctly represent that variables, while natural numbers can be avoided here.) Let $PHP_{n-1}^n$ state that $n$ pigeons can sit in $n-1$ holes, with each hole containing no more than one pigeon. So $PHP_{n-1}^n$ is the conjunction of the following clauses:
- $x_{i,1}\lor x_{i,2}\lor\cdots\lor x_{i,n-1}$ for $1\le i\le n$ (every pigeon sits in at least one hole);
- $\neg x_{i,k}\lor\neg x_{j,k}$ for $1\le i\ne j\le n,\,1\le k\le n-1$ (no two pigeons sit in the same hole).
Proving the pigeonhole principle is proving $PHP_{n-1}^n$ is unsatisfiable under any assignment of $x_{i,j}$'s.
A typical way to prove the principle is to use mathematical induction, i.e., by showing $PHP_{0}^1$ is unsatisfiable and if $PHP_{n-1}^{n-2}$ is unsatisfiable, then $PHP_{n-1}^n$ is unsatisfiable. However, mathematical induction relies on the definition of natural numbers, say, Peano's axioms. My question is: can we efficiently prove the pigeonhole principle without introducing such external definitions or axioms?
By "efficiently", I mean we had better not enumerate all possible assignments of $x_{i,j}$'s and show that each assignment is unsatisfiable, or something like that. In particular, a resolution proof is not considered to be an efficient proof, since Haken proved that for a sufficiently large $n$, any resolution proof of $PHP_{n-1}^n$ requires length $2^{\Omega(n)}$.
There is a variant of induction, a "downward" induction - we can see it at work at the four colors map theorem. A "killer" is the name for (one of) the smallest counter-example. If a map is a killer, the proof obtains a smaller map that is also "a killer", by also needing five colors. Also, the smallest maps have to be checked.
Suppose we have to prove that there is no bijection (one-to-one correspondence) between n pigeons and n-1 holes. We search for "a killer", the smallest counter-example. Suppose someone found a killer, say 1001 pigeons fits exactly in 1000 holes.
Then we REMOVE a pidgeon and its associated hole. What remains is a smaller counter example (contradiction !), a bijection between 1000 pigeons and 999 holes. Then we check 2 pigeons and 1 hole and we conclude that there are no such bijections, whatever finite n we consider.
This "downward induction" can not be discarded as a method. To count, in its very physical essence, is to remove one by one objects from some inbound stack.