The relation $<$ is not definable in the structure of the integers with successor function I have to prove the following statement:

Prove that there is no formula $\psi=\psi(x_0,x_1)$ in the language $\operatorname{Th}((\mathbb{Z},S))$ such that the relation $\{(m,n)\in\mathbb{Z}\times\mathbb{Z}: (\mathbb{Z},S)\models \psi[m,n]\}$ is a linear ordering of $\mathbb{Z}$. Conclude that the relation $<$ on $\mathbb{Z}$ is not definable in the structure $(\mathbb{Z},S)$

Notice that $S$ is the successor function and $\psi(x_0,x_1)$ a formula with two free variables. Can someone help me with this question because I have no idea how to solve this problem. I thought about quantifier elimination, but can you solve this also without quantifier elimination, for example with automorphisms?
 A: To use automorphisms to show no formula $\psi ( x,y )$ over the language $\{ S \}$ defines a linear order over $\mathcal{Z} = ( \mathbb{Z} , S )$, note, first, that since the only automorphisms of $\mathcal{Z}$ are the shifts we will not be able to work with $\mathcal{Z}$ itself, but rather some elementary extension.
Let's consider the structure $\mathcal{M} = ( \mathbb{Z} \cup \mathbb{Z}^* , s )$ where 


*

*$\mathbb{Z}^*$ is a "starred" copy of $\mathbb{Z}$ (disjoint from $\mathbb{Z}$);

*$s : \mathbb{Z} \cup \mathbb{Z}^* \to \mathbb{Z} \cup \mathbb{Z}^*$ is the naturally defined successor operator:  $$\begin{align} s ( n ) &= n+1 \\ s ( n^* ) &= (n+1)^*.\end{align}$$


It is fairly straightforward to show that $\mathcal{Z} \prec \mathcal{M}$, and so if $\psi (x,y)$ defines a linear order on $\mathcal{Z}$ it also defines a linear order, $\sqsubset$, on $\mathcal{M}$. Since the mapping $\sigma : \mathbb{Z} \cup \mathbb{Z}^* \to \mathbb{Z} \cup \mathbb{Z}^*$ defined by $$\begin{align} \sigma( n ) &= n^*\\ \sigma( n^* ) &= n\end{align}$$ is an automorphism of $\mathcal{M}$, it follows that for all $a,b \in \mathbb{Z} \cup \mathbb{Z}^*$ we have $$\mathcal{M} \models a \sqsubset b \quad \Leftrightarrow \quad \mathcal{M} \models \sigma(a) \sqsubset \sigma (b).$$
From this it is easy to show that both of the assumptions $0 \sqsubset 0^*$ and $0^* \sqsubset 0$ lead to contradictions.
(You can also see some previous related questions here and here.)
