Which axioms of the foundation of natural numbers are used in the proof of the pigeonhole principle? The pigeonhole principle is so obvious to me that I am not able to think of a proof based on the axioms of natural numbers. Can anyone please explain its proof clearly mentioning the axioms?
 A: It can be proved by induction; so the crucial axiom is that the natural numbers are well-ordered, that is, any nonempty set of natural numbers has a least element.
For a proof of the pigeonhole principle, see my answer to this other question. (Strictly speaking, what's proved there isn't exactly the pigeonhole principle - instead, it's the statement "There is no injection from a set of $n$ elements to a set of $m$ elements, if $n>m$" - but it's easy to get from this to the pigeonhole principle.)
A: Here is a non-numeric version of the pigeonhole principle that may interest you. The formal proof is too long to post here (several hundred lines, see "The Pigeonhole Principle" at my math blog).
Let $P$ be the (non-empty) set of pigeons, and $H$ the set of holes. Suppose each pigeon is put in a hole. Suppose further that there are more pigeons than holes, i.e. that no function mapping holes to pigeons is surjective (onto). 
Then at least two pigeons will be put in the same hole.
More formally:
$\exists a:a \in P\space\space$ i.e. there is at least one pigeon
$\implies \forall f:[f:P \to H\space \space\space$ i.e. each pigeon is put in a hole
$\land \forall g: [[g: H \to P]\implies g$ is not surjective] $\space \space$   i.e. there are more pigeons than holes
$\implies \exists b,c,d: [b\in P\land c\in P \land d\in H \land [b\ne c\land f(b)=d \land f(c)=d]]]\space \space$ i.e. at least two pigeons will be in the same hole.
