Infinitely many non-isomorphic models for the successor function I am trying to solve the following exercise:
Let $L=\{0,S\}$, where $0$ is a constant symbol and $S$ is an unary function symbol. Let $T$ be the set of following $L-$sentences.
\begin{align*}
& \forall x \forall y (S(x)= S(y) \rightarrow x = y) \\
& \forall y (y \neq 0 \rightarrow \exists x (S(x)=y)) \\
& \forall x (S(x) \neq 0) \\
& \forall x (S^n(x)\neq x) \quad , n \in \omega
\end{align*}
Show that $T$ has infinitely many pairwise non-isomorphic countable models.
We obtain a model $M$ for $T$ by setting $M := \{\mathbb{N};0_{\mathbb{N}},x+1\}$. We now have one of the infinitely many countable models. I shall use this as a starting point for all the others.
I want to define a model $M_n , n \in \omega$ over the universe $ \mathbb{N} \sqcup \mathbb{Z} \sqcup \dots \sqcup \mathbb{Z}$ with $n$ $\mathbb{Z}$'s. Then any $x \in M_n$ can be expressed as $x = (i_x, a_x), i \in \{0,...,n\}$ with the $a_x$ being a natural number for $i_x=0$ and an integer elsewise. The interpretation of the zero shall be $(0,0)$ and $S(i_x,a_x)=(i_x,a_x+1)$. Then $M_n$ models $T$.
It is left to show that the the $M_n, n\in \omega$ are pairwise non-isomorphic.
My approach is this: If I consider an ordering $<$ on $\mathbb{N}$ respectively $\mathbb{Z}$, I can show that the $M_n$ are pairwise non-order-isomorphic.
I introduce a well-ordering on each $\mathbb{Z}$ by $0,1,-1,2,-2,...$. Then the order type of $M_n$ is the sum of $n+1$ $\omega$'s, hence all the $M_n$ are pairwise non-order-isomorphic.
I am afraid however that this is not actually a solution.
Problem 1: $L$ does not contain a symbol for an order. Is it therefore even legitimite to create new structure in the form of an order? And even if it is, is there a way of showing the non-isomorphy using what is given with $L$ alone?
Problem 2: This is probably connected to problem 1. If all of what I have done is actually ok, is there any way of identifying the isomorphism of models to the isomorphism of order types? Because what I actually want is the first (i.e. a bijective mapping between the two universes, s.t. all the structure is being preserved).
Problem 3: If we order $\mathbb{Z}$ as indicated, we need to make sure that all elements but the zero have a predecessor (resp. are successors), so the successur function would have to move along $ \mathbb{N} \sqcup \mathbb{Z} \sqcup \dots \sqcup \mathbb{Z}$ by 
$0 \rightarrow 1 \rightarrow ...\rightarrow -m \rightarrow -m+1 \rightarrow ...0 \rightarrow 1 \rightarrow ...\rightarrow m \rightarrow m+1 \rightarrow ...\rightarrow-m, ...$
As opposed to the ordering $0,1,2,...,0,1,-1,2,...0,1,-1,...$.
Can this lead to complications?
Remark: I know that there are similar questions on the successor function, however the answers don't go into detail about the part with the non-isomorphic $M_n$.
Any help is appreciated.
Thank you.
 A: Let $M$ be a model of $T$, with $f$ the interpretation of the function symbol $S$.
If $a$ and $b$ are members of (the underlying set of) $M$, call $a$ and $b$ equivalent if there is a non-negative integer $k$ such that $b=f^{k}(a)$ or $a=f^{k}(b)$. This is an equivalence relation. In $M_n$, the number of equivalence classes is $1$ more than the number of copies of $\mathbb{Z}$.
Let $M$ and $M'$ be models of $T$, and let $\varphi$ be an isomorphism from $M$ to $M'$. Then $a$ is equivalent to $b$ if and only if $\varphi(a)$ is equivalent to $\varphi(b)$. Thus the cardinality of the number of equivalence classes is an isomorphism invariant, and therefore the $M_n$ are pairwise non-isomorphic.
Remark: It is legitimate to produce a partial order on any model of $T$, along the lines you described. And on your models, one can describe a total order, which though it has a somewhat arbitrary character, behaves reasonably well under isomorphism. 
For more general models of $T$, there are many non-isomorphic extensions of the natural partial order to a total order, so imposing such a total order is not  useful in discussing isomorphism and non-isomorphism. 
I do not understand the third problem. In any model of $T$, any equivalence class that does not contain the interpretation of $0$ has natural order isomorphic to the usual order on $\mathbb{Z}$. There is no reason to introduce a well-ordering, and no natural way to do so.
A: As André Nicolas's answer indicates, a simpler way to solve this problem is to use an equivalence relation, rather than an ordering.  Let me elaborate on what happens when you approach this problem using an ordering.
As alluded to in your Problem 1, if you introduce an ordering, you need to be sure that it is respected by isomorphisms.  That is, you can define an order $<$ on $M_n$, but to be able to use these orders to tell the $M_n$ apart, you would need to know that any isomorphism $f:(M_m,S)\to (M_n,S)$ is also an isomorphism of ordered sets $f:(M_m,<)\to (M_n,<)$.  Typically, the way you check a condition like this is by observing that $<$ is defined using the operation $S$ and no other structure of the sets $M_n$, and so it is routine to verify that a bijection preserving the operation $S$ must also preserve the relation $<$.  However, this is not obviously true in your case: your definition of $<$ uses your explicit description of the set $M_n$ as consisting of copies of $\mathbb{Z}$ (and $\mathbb{N}$), and is not stated in terms of the operation $S$.
In fact, it turns out that your order $<$ does not satisfy the condition above.  That is, there are isomorphisms between the structures $(M_n,S)$ that do not preserve the order $<$.  For instance, consider the map $f:M_1\to M_1$ given by $f(0,a)=(0,a)$ and $f(1,a)=(1,a+1)$.  This is a bijection that preserves $S$, but it does not preserve your ordering $<$, (for instance, $(1,0)<(1,-1)$ but $f(1,0)=(1,1)>(1,0)=f(1,-1)$).
So unfortunately, there is no apparent way to use your ordering to show the $M_n$ are not isomorphic.  However, you can use a different ordering.  Let me define a partial order $\prec$ on any model $M$ of $T$ as follows.  We say that $x\prec y$ if there exists a positive integer $n$ such that $y=S^n(x)$.  On $M_n$, this corresponds to the usual ordering on each $\mathbb{Z}$ (however, $\prec$ is not a total order if $n>0$, since elements in different copies of $\mathbb{Z}$ or $\mathbb{N}$ are incomparable).
Since $\prec$ is defined for any model of $T$ using only the operation $S$, it is easy to see that it is preserved by isomorphisms.  Explicitly, if $f:(M,S)\to (N,S)$ is an isomorphism of models of $T$ and $x,y\in M$, then if $x\prec y$ in $M$ then $x=S^n(y)$ so $f(x)=f(S^n(y))=S^n(f(y))$ so $f(x)\prec f(y)$ (and similarly conversely).
So if $M_n$ and $M_m$ are isomorphic, then the ordered sets $(M_n,\prec)$ and $(M_m,\prec)$ would be isomorphic.  But you can verify that $(M_n,\prec)$ is isomorphic to a disjoint union of one copy of $\omega$ and $n$ copies of $\mathbb{Z}$ (with their usual orders).  Since these partially ordered sets are not isomorphic for different values of $n$, the $M_n$ are not isomorphic for different values of $n$.  (But this raises the question of how you would actually prove that these partially ordered sets are not isomorphic, and to do so you would probably end up using the equivalence relation of André Nicolas's answer anyways.)
