[FOM] Dedekind's theorem

[meskew at math.uci.edu]

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.

Thanks,
Monroe