How does the Peano axiom of induction prevent S-loops? First, let me state what I understand to be the first-order rendition of Peano's 5th axiom: the axiom of induction.
For all natural numbers, for any relation/property/predicate $R$...
$$(R(0) \land \forall x[R(x) \rightarrow R(S(x))]) \rightarrow \forall x(R(x))$$
(first question: is this a correct formalization of this axiom or not?)
How does this axiom prevent elements of natural numbers that have '$S$-loops' that is: 
\begin{align}
S(a) = b
&& \text{and} &&
S(b) = a
\end{align}
(edited for clarity)
 A: Using Peano's axioms 
\begin{align}
\forall m \, S(m) \neq 0 &&&\text{(}0\text{ is not the successor of anyone)}
\\
\forall m \forall n \, (S(m) = S(n) \to m = n) &&&\text{(injectivity of }S\text{)}
\end{align}
and Peano's principle of induction, it is easy to prove that the "double-successor" does not have any fixed point, i.e.
\begin{align}
\forall m \, S(S(m)) \neq m
\end{align}
A rigorous proof of this property is below. It is analogous to the one you can find here to prove that the successor has no fixed point. 
Now, this property excludes the possibility of $S$-loops. Indeed, if there were $m$ and $n$ such that 
\begin{align}
S(m) &= n & S(n) &= m
\end{align}
then we would have $S(S(m)) = m$ (replace $n$ with $S(m)$ in the second identity), which is impossible.

We want to prove that, in Peano arithmetic,
\begin{align} 
\forall x \, S(S(x)) \neq x &&&\text{(i.e. } \forall x \, R(x) \text{ where } R(x) \text{ is the formula } S(S(x)) \neq x\text{).}
\end{align}
To prove this we apply Peano's induction principle, thus we have to prove two facts:


*

*Base case, i.e. $S(S(0)) \neq 0$. This holds because it is just an instance (take $x = S(0)$) of Peano's axiom 
\begin{align}
\forall x \, S(x) \neq 0 &&&\text{($0$ is not the successor of anyone).}
\end{align}

*Inductive case, i.e. $\forall x \, \big(S(S(x)) \neq x \to S(S(S(x))) \neq S(x) \big)$.
So, given $x$, we suppose $S(S(x)) \neq x$ and we have to show that $S(S(S(x))) \neq S(x)$.
Aiming for a contradiction, suppose $S(S(S(x))) = S(x)$.
According to Peano's axiom 
\begin{align}
\forall m \forall n \, (S(m) = S(n) \to m = n) &&&\text{(injectivity of }S\text{)}
\end{align}
instantiated with $m = S(S(x))$ and $n = x$, we have that $S(S(x)) = x$, which is impossible.
Therefore, $S(S(S(x))) \neq S(x)$.
This ends the proof that $\forall x \, S(S(x)) \neq x$.
A: I think your formalization is correct.
The axiom of induction doesn't prevent by itself S loops. Consider, a two elements set $\{0,1\}$ with $S(0) = 1$ and $S(1) = 0$ 
To prevent S loops you need axioms
4."Two numbers of which the successors are equal are themselves equal."
$$ \forall a,b \; . \; S(a) = S(b) \Rightarrow a = b $$ 
3."$0$ is not a succesors"
$$ \forall a\;.\;S(a)\neq0 $$
Informally, if you have a loop from combination of (5) and (4) it follows that loop need to involve all predecessors of a looped element. And with this (3)  provides a contradiction, as by (5) every element has $0$ as a predecessor. 
The more formal proof can look like this.
Consider the predicate
$$NL(x) = \text{$x$ is not an element of any loop.} $$
By definition of the loop, if $a$ is in the loop, there must be $b$ in the loop, such that $a = S(b)$. So, $NL(0)$ holds by axiom (3). Now consider an element $a$ such that $NL(a)$ holds. If $S(a)$ is an element of the loop, then by the axiom (4) the element $a$ is also in the loop. This is a Contradiction! Thus, $NL(a) \Rightarrow NL(S(a))$ holds for any $a$. Now can apply axiom of induction to see that there is no element $a$, which can be looped. 
So there are no loops in Natural numbers defined by Peano axioms. Note, however, that you need every axiom to prove it.
A: In the general statement as you’ve now written, not a specific example as you had before, induction does come into play in the sense that one must prove, by induction, that if $x\in \mathbf{N}$, then either $x=0$, or there exists $k$ such that $x=S^k(0)$. 
Indeed you let the property by “$x=0$ or $x$ is a descendant of $0$”; $0$ has the property, and if $n$ has the property, then so does $S(n)$. 
Once you have that, from $S(a)=b$ and $S(b)=a$, you get that either $a=0$ and you violate the Axiom that says that $0$ is not a successor; or else that $a=S^k(0)$ for some $k$. Then $b=S^{k+1}(0)$, and you are now in essentially the same situation as before, when you had the specific example of $S(x_8)=x_9$ and $S(x_9)=x_8$. Now you have $S^{k+2}(0)=S^k(0)$. From that you get $S^{k+1}(0)=S^{k-1}(0)$, and so on until you get that $0$ is a successor, contradicting that axiom.
A: @Taroccoesbrocco,
so in the spirit of a 'double successor' implies contradiction, would a formalization of this look like:    


*

*Let R(x) -> S(S(x)) = x   (double successor relation)    

*By Axiom 5 then R must also apply to $0$    

*So $S(S(0)) = 0$    

*Let $a = S(0)$    

*By 4 and 3, $S(a) = 0$...which contradicts Peano Axiom 4    

*Therefore relation R (ie...double successor) is not in the natural numbers.   


Is there anything incorrect about the above line of reasoning?
