**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.