Here's Dedekind's definition:
A set $S$ is said to be infinite if there is an injection from $S$ to one of its proper subsets.
There is a hidden other half implied by this definition, namely that a finite set is one that is not infinite. One might imagine that it also says:
A set $S$ is said to be finite if there is no injection from $S$ to any of its proper subsets.
Or equivalently:
There is no injection from a finite set $S$ to one of its proper subsets.
Or equivalently:
If $f$ is a mapping from a finite set $S$ to one of its proper subsets, then $f$ is not an injection
Replacing "injection" with its definition:
If $f$ is a mapping from a finite set $S$ to one of its proper subsets, there are distinct $x$ and $y$ in $S$ with $f(x) = f(y)$
Now comes what I think is the only leap: imagine that the elements of $S$ are the pigeons, and that the pigeonholes are also labeled by elements of $S$. But not every possible element of $S$ is a label, so that the set of labels is a proper subset of $S$. Then the function $f$ says, for each pigeon, which hole it goes into:
If $f$ is a mapping from a finite set of pigeons $S$ to a set of pigeonholes labeled with elements of a proper subset of $S$,there are distinct pigeons $x$ and $y$ with $f(x) = f(y)$
Or equivalently:
If $f$ sends pigeons from a finite set $S$ to a set of pigeonholes labeled with elements of a proper subset of $S$, there are distinct pigeons $x$ and $y$ sent to the same hole
I think this is the version of the pigeonhole principle that Kanamori was thinking of.
There's still a piece missing before we get to your version of the pigeonhole principle, which is that finite sets have sizes, which are numbers. To do this properly is a little bit technical.
We define a number to be one of the sets $0=\varnothing, 1=\{0\}, 2=\{0, 1\}, 3=\{0, 1, 2\}, \ldots$. We can define $<$ to be the same as $\in$, or perhaps the restriction of $\in$ to the set of numbers. For example, $1<3$ because $1\in 3 = \{0,1,2\}$.
Then we can show that for any finite set $S$ there is exactly one number $n$ for which there is a bijection $c:S\to n$, and we can say that this unique number is the size $|S|$ of set $S$. Then we can show that if $S$ and $S'$ are finite sets with $S'\subsetneq S$, then $|S'|<|S|$.
Once this "size" machinery is in place, we can transform the statement of the pigeonhole principle above from one about a set and its proper subset to one about the sizes of the two sets:
If $f$ sends pigeons from a set of size $s$ to a set of pigeonholes of size $s'$, with $s'<s$, there are distinct pigeons $x$ and $y$ sent to the same hole
Or, leaving $f$ implicit:
If pigeons are sent from a set of size $s$ to a set of pigeonholes of size $s'$, with $s'<s$, there are distinct pigeons $x$ and $y$ sent to the same hole
Which is pretty much what you said:
If $s$ items are put into $s'$ pigeonholes with $s > s'$, then at least one pigeonhole must contain more than one item.
I hope this is some help.
Best Answer
As the wikipedia article describes, Dirichlet's approximation theorem is a foundational result in diophantine approximation. For a real number $x$, let $\|x\|$ denote the distance from $x$ to its closest integer. Then the theorem states that for any irrational number $\alpha$, there exists infinitely many $q \gt 0$ such that $$ \| q\alpha \| \leqslant \frac{1}{q}. $$ This theorem is a simple consequence of the pigeonhole principle, and I was very surprised on seeing the proof. You can find the proof in robjohn's answer to the question: Approximation of irrationals by fractions.
In words, this theorem says that we can approximate the irrationals as closely as we want (in the sense of $\| q \alpha \|$) if we are allowed to pick a large enough $q$. This may not sound that surprising at first, but it becomes striking when one compares it to rational case.
Suppose $\alpha = a/b$ where $a$ and $b$ are integers and $b \geqslant 1$. We want to know how well $\alpha$ can be approximated using other rationals, since otherwise the problem is trivial. So fix $p/q \neq \alpha = a/b$. Rearranging, $qa - pb$ is nonzero; since it is also an integer, $|qa - pb|$ must be at least $1$. Thus, $$ |q\alpha - p| = \frac{|qa - pb|}{b} \geqslant \frac{1}{b}. $$ In particular, if $q \alpha$ is not an integer, then $\| q \alpha \| \geqslant \frac{1}{b}$, which is bounded away from zero, irrespective of $q$.
Thus, in a precise sense, the irrational numbers can be better approximated using rationals than the rational numbers themselves! (Of course, as stated previously, in the rational case, we do not count "approximating" the number by itself.)