Prove $x' \neq x$ using Peano axioms I am looking at Edmund Landau, Foundation of analysis and do not agree with is proof of Theorem 2 part 2. I put the pages here for easy reference (http://pbrd.co/1y89p7b and  http://pbrd.co/1y89A2s). 
Problem I have with Landau, is theorem 2,  part 2  does not prove the theorem (I think). 
Theorem is \begin{equation}x’ \neq x\end{equation} 
1. He assumes the theorem and goes on with the result.


*Another issue, if we assume successor function is injective does not mean that x and suc(x) can be one and the same in value. Lastly, injection is a big assumption. Axiom 2 “exactly 1” but does not say mutually exclusive.

*I have a separate proof via contradiction. Basically I assume x’ = x and using axiom 4, disprove it as below:
Assume
\begin{equation}x’ = x\end{equation} 
Also,from Axiom 4
\begin{equation} 
x' = y' => x = y
\end{equation} 
This leads to the following contradiction from our assumption and 1st part of axiom 4 that:
\begin{equation}
x = y'
\end{equation} 
This cannot be true because of part 2 of axiom 4 which says:
\begin{equation}
x = y
\end{equation} 
Since the axiom must hold true making our assumption as incorrect. Hence the theorem is proved i.e.
\begin{equation} 
x' \neq x
\end{equation} 
Would appreciate any insights. Is it because this book is a translation of the original german book and someone messed it up ?
 A: I'll try only to recap André's comments regarding Landau's proof : there are no mistakes in the book's translation from the original german edition.
Theorem 2 [page 3] : $x' \ne x$
Note : with more details, Landau will prove : for all $x$, $(x' \ne x)$.
The proof is by induction; thus, we have to review [page 2] :

Axiom 5 (Axiom of Induction) : Let there be given a set $\mathfrak M$ of natural numbers, with the following properties :

I) $1$ belongs to $\mathfrak M$ 
II) if $x$ belongs to $\mathfrak M$ so does $x'$.

Then $\mathfrak M$ contains all the natural numbers.

Now for the proof of Th.2 :

Let $\mathfrak M$ the set of all [natural numbers] $x$ for which $x' \ne x$ hold true.

First, we have to prove the basis of induction :

I) By Axiom 1 and Axiom 3 : $1' \ne 1$; therefore $1$ belongs to $\mathfrak M$.

We have :

Axiom 1 [page 2] : $1$ is a natural number.

Thus, $1$ is a "candidate" for being one of $x$ belonging to $\mathfrak M$.

Axiom 3 [page 2] : We always have : $x' \ne 1$.

This means that : for all [natural numbers] $x$, $(x' \ne 1)$; thus, being $1$ a natural number, we have : $1' \ne 1$.
So far, we have proved step I) of Axiom 5 : $1$ belongs to the set $\mathfrak M$ of all [natural numbers] $x$ for which $x' \ne x$ hold true.
Now for the induction step :

II) If $x$ belongs to $\mathfrak M$, then $x' \ne x$, and hence by Theorem 1, $(x')' \ne x'$, so that $x'$ belongs to $\mathfrak M$.

This is the "standard" induction step : assume $A(n)$ and prove $A(n+1)$. In Landau's proof :

assume $x' \ne x$ and prove $(x')' \ne x'$ 

and this is proved according to :

Theorem 1 [page 3] : if $x \ne y$, then $x' \ne y'$,

with $x'$ in place of $x$ and $x$ in place of $y$.
Conclusion : 


*

*Let $\mathfrak M$ the set of all [natural numbers] $x$ for which $x' \ne x$ hold true. 

*By I) we have proved that : $1$ belongs to $\mathfrak M$. 

*By II) we have proved that : if $x$ belongs to $\mathfrak M$, then $x'$ belongs to $\mathfrak M$.

*Now we can apply Axiom 5 to conclude with : 


$\mathfrak M$ contains all the natural numbers,


which amounts to saying that :

for all $x$ , $x \in \mathfrak M$, i.e. for all [natural numbers] $x$, $x' \ne x$ hold true. 


Note that Landau follows quite closely Peano's original formulation; see :


*

*Giuseppe Peano, Arithmetices principia, nova methodo exposita (1889: The principles of arithmetic presented by a new method), in Jean van Heijenoort, From Frege to Gödel : A Source Book in Mathematical Logic (1967), page 94.

A: Base Case:
$$0' \ne 0$$
That is an axiom: nothing precedes $0$.
Inductive case:
$$\begin{align}
x' \ne x & \Rightarrow x'' \ne x' &\text{Inductive Statement} \\
x'' = x' &\Rightarrow x' = x  & \text{Contrapositive} \\
y' = x' &\Rightarrow y = x  & \text{by letting y =  x'} \\
\end{align}$$
That is also an axiom:  Successor is injective (invertible).
And induction is itself an axiom.
