Is Pigeonhole Principle the negation of Dedekind-infinite?

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.

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.

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.