Is Pigeonhole Principle the negation of Dedekind-infinite? From Wiki, "The Pigeonhole Principle":

In mathematics, the pigeonhole principle states that if n items are
  put into m pigeonholes with n > m, then at least one pigeonhole must
  contain more than one item.

From "The Mathematical Infinite as a Matter of Method," by Akihiro Kanamori:

In 1872 Dedekind was putting together Was sind und was sollen die
  Zahlen?, and he would be the first to define infinite set, with the
  definition being a set for which there is a one-to-one correspondence (bijection?)
  with a proper subset. This is just the negation of the Pigeonhole
  Principle. Dedekind in effect had inverted a negative aspect of finite
  cardinality into a positive existence definition of the infinite.

How can this be? Dedekind's definition of infinite makes no reference to natural numbers or any kind of ordering:
A set $X$ is Dedekind-infinite iff there exists a proper subset $X'$ of $X$ and bijection $f:X'\rightarrow X$  
See follow-up in my answer below.
 A: Yes. 
Finiteness as defined by Dedekind is exactly the assertion "the pigeonhole principle holds", that is every self-injection is a surjection. 
The whole idea is to use this property to define what is finite and what is infinite.
A: It's not clear what you mean by your objection. Dedekind's definition doesn't use the natural numbers, but that doesn't mean we can't use induction to show that we can find $n$ distinct elements of $X$ for any natural number $n$.  
If what you mean is that Dedekind hasn't defined "finite," that is true. The Pigeonhole Principle is an intuitively true theorem, but to prove it rigorously, we'd need a definition of finite. What Dedekind is doing is saying, "Let's use the pigeonhole principle as our definition for 'finite set.'") That is, an infinite set is one that does not satisfy the pigeonhole principle. 
The intuition for this is that an infinite set $X$ contains a countable infinite subset, $\{x_1,x_2,\dots\}$. In which case, we can define $X'=X\setminus \{x_1\}$ and define $f(x)=x$ if $x\not\in \{x_1,\dots\}$ and $f(x_n)=x_{n+1}$. Again, that is an intuition, since we don't actually have an alternative definition other than Dedekinds for "infinite" at this point to compare his with.
A: You need not reference the natural numbers to state the Pigeonhole Principle. It could just as well be stated that there is no injection from a finite set to any of its proper subsets. The thing we usually call the Pigeonhole Principle ($n$ pigeons and $m$ holes with $n > m$) would become a special case.
A: In line with MJD's answer -- except you don't need to refer to the sizes of sets...
The original pigeonhole problem is one of mapping a finite set of pigeons $P$ to a smaller set of holes $H$, the size of a set being given the number of elements in it. 
To apply the definition of Dedekind-finiteness, we must recast the problem as one involving a finite set $S$, a proper subset $S'$ of $S$, and a subset $S''$ of $S'$ where $S$ corresponds to P in the original problem, S' corresponds to H and S'' corresponds the set of occupied (non-empty) holes. 
$S''\subset S' \subset S$
By "corresponds to," I imply the existence of a bijection to sets of "labels," $S$, $S'$ and $S''$ where $S$ is the set of labels assigned to elements of $P$, $S'$ is the set of labels assigned to the elements of $H$, and $S''$ is the set of labels assigned to non-empty holes. Note that a pigeon and a hole may have the same label in this setup. And that the pigeon labelled $x$ may or may not be assigned to the hole labelled $x$. (It can get messy! Is there a more elegant way?) 
Using Dedekind-finiteness then, we can then prove that for any function $f$ mapping mapping $S$ onto $S''$,  there exists distinct $x$ and $y$ in $S$ such that $f(x)=f(y)$, i.e. there must be at least two pigeons in at least one hole. 

FOLLOW-UP (2 years later)
It turns out that, for any non-empty (not necessarily finite) set of pigeons, if there exists no surjection mapping pigeonholes to pigeons, then there must be at least two pigeons in the same hole. See my formal proof in the posting "The Pigeonhole Principle" at my math blog.
A: Back in the 1970's, when I was working on programming verification using Pascal and a mechanization of Hoare's axioms,
I tried to prove the following program (or its equivalent in Pascal with assertions) correct:
function php(n: int, f:maps [0:n] to [1:n]) returns (int, int);
for{i=0 to n-1} for{j=i+1 to n} if (f(i) == f(j) ) return (i, j);
return (0, 0);
Essentially, this is an implementation of the pigeon-hole principle.
The key is that the input is a function (f) that maps
[0 to n] to [1 to n]
so that there are distinct i and j such that
f(i) = f(j); this program finds tham.
The problem was to insert the proper assertions in the program
and use the verification generator to prove that the "return(i, j)"
would always eventually be taken.
I eventually managed to do it,
but the theorems involved were far beyond the capabilities
of the theorem prover available then.
I proved them by hand with a lot of effort.
I know that this isn't a proper answer to the question,
but it is somewhat relevant.
Along the same lines,
I also wrote a version of this function
which cached the function values
so the time would be O(n) instead of
O(n$^2$).
The assertions for this version were more complex
and I was not able to prove its correctness.
A: 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.
