Peano's Axiom: Is it implied that successor of a number is not the number itself?

Question

Using the Peano's Axioms from MathWorld as the basis, I'm wondering if it is implied that the successor of a number is not the number itself, or is it deducible?

Answer 1

We can formalize these Peano's Axioms in first-order logic as follows:

$\forall x \ s(x) \not = 0$ (this is Peano axiom 3)

$\forall x \ \forall y \ (s(x) = s(y) \rightarrow x = y)$ (this is Peano Axiom 4)

for any formula $\varphi(x)$:

$(\varphi(0) \land \forall x (\varphi(x) \rightarrow \varphi(s(x)))) \rightarrow \forall x \ \varphi(x)$ (this is a general scheme that captures Peano Axiom 5 ... $S$ would be the set of all objects for which $\varphi(x)$ is true)

Using this, you can derive the statement $\forall x \ s(x) \not = x$, i.e. that the successor of any number is never that number itself: