Is induction neccessary for proving that every injective mapping of a finite set into itself is a mapping onto itself?

Upon reviewing the basic theorem that the number of elements in a fixed finite set is unique, I tried to determine what part of this proposition is in need of proof. It seems axiomatic. Nonetheless, BBFSK have a very long-winded, and seemingly convoluted discussion of this, and related ideas.

When I attempted to produce my own argument in support of the above proposition, the part which I am not able to state purely in the terminology of mappings (bijection, injection, etc) is that an injection of a finite set into itself is a mapping onto itself. The proof BBFSK give uses induction. After thinking about it for a while, that was the only approach I could come up with.

Is there a rigorous proof of the proposition that every injective mapping of a finite set into itself is a mapping of the set onto itself which does not involve induction?

Dedekind proposed to use this property as the definition of "finite set", so that's at least one alternative -- closely in line with your intuition of declaring it to be axiomatic. Unfortunately there are technical problems with that approach. In particular you then need the axiom of choice to prove that induction works for all "finite" cardinalities, which is untidy at the least.

(A set $$X$$ such that every injection $$X\to X$$ is a bijection is now called "Dedekind-finite").

In a standard development of set theory, on the other hand, you're out of luck. Here "finite" is defined as "has the same cardinality as an element of $$\omega$$", and $$\omega$$ is (essentially) defined to be the largest set that mathematical induction works for. So in order to prove anything about "finite" you need to have an induction somewhere, because that's the only way to connect to the definition. This induction can be hidden in the proof of another property that you depend on, but that is basically just kicking the buck around. Eventually it has to stop.

This comment by Daniel Schepler is also relevant (but see further discussion in the comment thread):

There's also the notion of Kuratowski finiteness, which is essentially equivalent to the condition that the power set of $$𝑋$$ is well-founded under the relation of "strict extension by one element". But then, of course, the natural way to prove nearly anything about Kuratowski finite sets is to use induction on the well-foundedness property...

• The definition the authors give is that a finite set is one which can be put in one-to-one correspondence with a segment $A_n=\left\{x\in\mathbb{N}|1\ge x \le n\right\}.$ It appears that what we are saying amounts to "if you count a set of objects, rearrange them, then count them again, you'll get the same number". – Steven Thomas Hatton Apr 30 at 20:54
• @StevenHatton: That's the same definition as the one Henning provides, because in the "usual" construction of $\mathbb{N}$ as an inductive set, your $A_n$ is exactly equal to $n+1$ (modulo including $0$ in $\mathbb{N}$)... – Arturo Magidin Apr 30 at 20:58
• @StevenHatton: To be more explicit; in the "usual" construction as an inductive set, we have $0=\varnothing$, $n^+ = n\cup\{n\}$ for any set $n$, and $\mathbb{N}$ is the smallest set that includes $0$ and such that if $x\in\mathbb{N}$ then $x^+\in\mathbb{N}$. Then $1=0^+$, $2=1^+$, etc., and in this construction, the set $n$ contains exactly $n$ elements, namely $0,1,2,\ldots,n-1$. – Arturo Magidin Apr 30 at 21:06
• Bu the way: @Arturo gives the usual textbook definition of $\mathbb N$ (a.k.a. $\omega$). My characterization as "the largest set induction works for" looks rather different at first, but is nevertheless what the textbook definition achieves. Because $\omega$ contains $0$ and all the $x^+$s, induction must fail in any _strictly larger_ set (as $\omega$ itself would be a counterexample) -- and being the "smallest set" that satisfies this exactly guarantees that induction will work in $\omega$. – Henning Makholm Apr 30 at 21:21
• There's also the notion of Kuratowski finiteness, which is essentially equivalent to the condition that the power set of $X$ is well-founded under the relation of "strict extension by one element". But then, of course, the natural way to prove nearly anything about Kuratowski finite sets is to use induction on the well-foundedness property... – Daniel Schepler Apr 30 at 21:37