Infinite natural numbers? Only using the successor function $\nu$ and the other axioms, how do we guarantee that the "next" generated number is different from all the "previous" numbers (I am using quotations because we havent defined order yet)? Concrete example: Prove that 3 is different from all "previous" numbers.
$$0\neq \nu(\nu(\nu(0)))$$
This is true by axoiom 4. Now we prove that $1\neq3$
$$\nu(0) \neq \nu(\nu(\nu(0)))$$
by injection axiom of $\nu$ we get
$$ 0 \neq \nu(\nu(0))$$
And by axoiom 4, this is a true statement. Now we could prove $2\neq3$ but i think my point is clear. We just "peel" off $\nu$ until we arrive at some form of $0 \neq \nu(*)$. I don't see how one would prove this generally, that every "next" generated number is different from all the  "previous" ones without really defining order. But in order to define order we need to guarantee that every "next" generated number is different from the previous ones hence we are looping around.
I still gave it a go and came up with some kind of "proof"
$$ 0 \neq \nu(m) \ , \ \forall m \in \mathbb{N}$$
This is guaranteed by axiom 4. And now by applying the $\nu$ "as often as you want" to both sides we allways obtain that both sides are not equal due to injection.
 A: Note that the injection axiom along with the fact that $0$ is not in the image of the successor function tells us that for any model of Peano Aritmetic ($PA$) has to be infinite since there will always be an injection to a proper subset. Note this is a meta theory observation since $PA$ can't say things of cardinality nor of successor loops as mentioned before. Weren't it for the Axiom scheme of induction you wouldn't be able to prove that there aren't any successor loops. This is because $Q$ (Peano minus Induction) has models that have loops (one model is the natural numbers with two other elements). You can express the fact that the successor function doesn't loop around with a theorem scheme. Or rather you can prove for all $m\in \mathbb{N}$ (this is a meta theory number) using induction  the following $\forall n \; n\neq S^m(n)$. The proof is the one you did but notice you can't quantify $m$ since $S^m$ is a short hand for the successor symbol repeated $m$ times so $m$ is not a term. What you end up with is showing in the meta theory that for all $m$ $PA$ proves that there can't be an $m$ successor loop.
A: If, like most number theorists, you are not constrained to first-order PA, there is a much easier way to prove the infinitude of the natural numbers. It is a trivial application of the definition of a Dedekind infinite set. Hint: The required bijection is $f:N\to N \setminus \{0\}$ such that $f(x)=S(x)$ where $S$ is the usual successor function on $N$ from Peano's Axioms.
A: You can, just with the Peano Axioms, prove (a version of) the recursion theorem, with that you can define $f^n$ via $ f^0=id_A$$\\$ $f^{\nu(n)}=f^n \circ f$, where f is $f:A\to A$.
With that you can show that "the next generated number, starting at $0$" is different from the previous ones.
