# The relation < is not definable in the structure of the integers with sucessorfunction

I have to prove the following statement:

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

Notice that $S$ is the sucessor 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 QE, but can you solve this also without QE, for example with automorphisms?!

Thank you for help :)

-

Hint: To use automorphisms, you will probably have to move to an elementary extension of $\mathcal{Z} = ( \mathbb{Z} , S )$ (since the automorphisms of $\mathcal{Z}$ are just shifts). Try looking at the structure $\mathcal{M} = ( \mathbb{Z} \cup \mathbb{Z}^* , s )$ where
• $\mathbb{Z}^*$ is just a "starred" copy of $\mathbb{Z}$ disjoint from $\mathbb{Z}$; and
• $s$ is defined by $s ( n ) = n+1 = S(n)$ for $n \in \mathbb{Z}$, and $s( n^* ) = (n+1)^* = (S(n))^*$ for $n^* \in \mathbb{Z}^*$.
If $\varphi (x,y)$ defines a linear order in $\mathcal{Z}$, it also defines a linear order, $\prec$, in $\mathcal{M}$. Use the obvious automorphism of $\mathcal{M}$ to show that the assumptions $0 \prec 0^*$ and $0^* \prec 0$ both lead to contradictions.
@CountableUniversal: I believe that quantifier elimination should work, provided you can show that $\mathrm{Th} ( \mathbb{Z} , S )$ admits quantifier elimination. I might be incorrect on some specifics (or even some generalities) but if $\varphi (x,y)$ is quantifier-free then there should be a bound $N$ (likely one more than the number of occurrences of $S$ in $\varphi$) such that given $m_1,n_1,m_2,n_2 \in \mathbb{Z}$ if $| m_1 - n_1 | , | m_2 - n_2 | \geq N$, then $\mathcal{Z} \models \varphi (m_1,n_1)$ iff $\mathcal{Z} \models \varphi (m_2,n_2)$. –  Arthur Fischer Nov 16 '12 at 15:18