Question

In "Was sind und was sollen die Zahlen?" Dedekind gives a noncircular proof of the statement that a set is finite if and only if it cannot be put in bijective correspondence with a proper subset.  By "circular" I mean in this context that you should not prove it by simply saying that a proper subset of a finite set will have a smaller cardinality; this theorem should be taken as the ground for the well-definedness of the finite cardinals.

Regarding the "only if" direction, which establishes that finite ordinals are cardinals, was Dedekind the first to publish a proof of this?  Did Frege give a proof independently?  Galileo?  Leibniz?  Some medieval monk perhaps?  It would seem strange if this basic aspect of the concept of number was not reflected upon for so many centuries.

Answer 1

Regarding the narrower interpretation of your question, the fact that the finite numbers are not equinumerous with any proper subset is also expressed as the classical pigeon hole principle. And for this, the linked Wikipedia article asserts that "the first formalization of the idea is believed to have been made by Johann Dirichlet in 1834 under the name Schubfachprinzip (drawer principle or shelf principle)," and this of course pre-dates Dedekind.

One can easily prove it by induction on $n$, for if $n$ is a minimal counterexample, with $f:n\to n$ injective but not surjective, then one can easily construct a smaller counterexample by considering and rearranging the action on one point.

Answer 2

EDIT NOTE: Thanks to Asaf Karagila for pointing out an error in the previous set-up; now the emphasis is put on finiteness vs Dedekind finiteness.

The notion of a finite ordinal is quite modern, and was only articulated after Cantor's invention of set theory and his investigations of various kinds of linearly ordered sets, especially well-ordered ones. Also

Moreover, in our modern axiomatic view of set theory, Dedekind's characterization of finiteness only works in the presence of the axiom of choice.

More specifically, let us define a set $X$ to be Dedekind finite provided there is no bijection between $X$ and a proper subset of $X$; and to be finite iff there is no $n \in \Bbb{N}$ such that $X$ has cardinality $n$. We also define $X$ is infinite iff $X$ is not finite. Then we have:

(1) The implication "If $X$ is finite, then $X$ is Dedekind finite" is provable in $ZF$ (Zermelo-Fraenkel set theory without the axiom of choice). This implication is one of the versions of the Pigeon-hole principle (see Joel Hamkins' answer).

(2) The implication "If $X$ is Dedekind finite, then $X$ is finite" is provable in $ZFC$ = $ZF$ + $AC$ [the axiom of choice].

(3) However, the implication "If $X$ is Dedekind finite, then $X$ is finite" is not provable in $ZF$. This was established first by Paul Cohen, in the early 1960's, as one of the first impressive exhibits of his "forcing" technology. Indeed, as shown by Cohen, in the absence of the axiom of choice, it is possible to have an infinite Dedekind finite subset of $\Bbb{R}$. It is not hard to see that $X$ is not Dedekind finite iff $\Bbb{N}$ can be injected into $X$; so in Cohen's model there is an infinite subset of $\Bbb{R}$ into which $\Bbb{N}$ cannot be injected.

Finally, according to the source below [p.45, footnote 4], Dedekind's definition was also independently proposed by C.S. Pierce.

Fraenkel, Abraham A.; Bar-Hillel, Yehoshua; Levy, Azriel Foundations of set theory. North-Holland, 1973.

PS. Euclid's "the whole is greater than a part" - one of the five "common notions" in the Elements - might be been argued to be a precursor of Dedekind's theorem. Also, the idea of reducing the notion of cardinality to 1-1 correspondences is referred to as Hume's Principle in some modern philosophical texts, based on Frege's attribution of the principle to the 18th century philosopher David Hume.

Answer 3

Bolzano's work on paradoxes of the infinite may be relevant in this context.