Help me understand the proof that usual ordering $\leq$ is not first-order definable in the structure $\left(\mathbb{N};s\right)$. Here is the outline of the proof, given by spaceisdarkgreen:


*

*The models of $Th(\mathbb{N},s)$ consist of a copy of $\mathbb{N}$ and any number of copies of $\mathbb{Z}$. 

*For any two elements in different copies of $\mathbb{Z}$ there is an automorphism swapping them. 

*This means there are models of $Th(\mathbb{N},s)$ in which we cannot define an ordering (or more generally any total antisymmetric relation). 

*If we could define an ordering in $(\mathbb{N},s)$ the formula would define an ordering in any model of its theory.
Here is what (I think) I understand. The set $\mathbb{N}$ and the function $s$ are axiomatized by Peano axioms:


*

*$0\in\mathbb{N}$

*$\forall x\left[x\in\mathbb{N}\rightarrow s(x)\in\mathbb{N}\right]$

*$\forall x\left[x\in\mathbb{N}\rightarrow\neg0=s(x)\right]$

*$\forall x\forall y\left(x,y\in\mathbb{N}\rightarrow\left[x=y\leftrightarrow s(x)=s(y)\right]\right)$

*$\forall K\left(0\in K\wedge\forall x\left[x\in K\rightarrow s(x)\in K\right]\rightarrow\mathbb{N}\subseteq K\right)$
Let call $\mathcal{PA}$ the set of the above statements. Then, theory $Th(\mathbb{N},s)$ is the set of all the sentences $\phi$ such that $\phi$ is a consequence of $\mathcal{PA}$: 
$Th(\mathbb{N},s)=\{\phi|\mathcal{PA}\vdash\phi\}$
Models of $Th(\mathbb{N},s)$, are the structures that satisfy it's sentences. A structure has a domain $D$. The domain of a model of $Th(\mathbb{N},s)$ must contain $\mathbb{N}$, otherwise it cannot satisfy the sentences of $Th(\mathbb{N},s)$. But $D$ could contain other things also. Since $s$ must be a total function, for $x_{i}\notin\mathbb{N}$ we may also have:
• Other infinite sequences of objects with an initial element $x_{0}$: $s(x_{0})=x_{1},s(x_{1})=x_{2},...$
• Infinite sequences without an initial element: $...s(x_{i})=x_{i+1},s(x_{i+1})=x_{i+2},...$
• Circles: $s(x_{0})=x_{1},s(x_{1})=x_{2},...s(x_{n})=x_{0}$
• Finite sequences like $s(x_{0})=x_{1},s(x_{1})=x_{2},...s(x_{n})=x_{n}$ 
e.t.c.
Now, I'm not sure about the meaning of the expression “structure $\mathbb{N}+\mathbb{Z}+\mathbb{Z}$”, mentioned by Noah Schweber here, and either for spaceisdarkgreen's statement, “The models of $Th(\mathbb{N},s)$ consist of a copy of $\mathbb{N}$ and any number of copies of $\mathbb{Z}$”, in the comments. Surelly here “$+$” does not mean union, otherwise $\mathbb{N}+\mathbb{Z}+\mathbb{Z}=\mathbb{Z}$. And surelly $D$ can not have more than one copy of each of it's elements. So, I guess, what is meant is that, along with $\mathbb{N}$, we may also have two or more infinite sequences of the form $...s(x_{i})=x_{i+1},s(x_{i+1})=x_{i+2},...$ (which is of the same form as the sequence of integers). 
If the above is correct, then, obviously, Peano axioms cannot define an ordering relation that holds for objects that are not in $\mathbb{N}$, because if we rearrange them, the sentences of $Th(\mathbb{N},s)$ will still hold. PA do not say anything about these objects anyway. But, let “$\leq$” holds only for elements of $\mathbb{N}$. What is the problem with that? And why then “the formula would define an ordering in any model of its theory”? 
Or, equivalently, suppose we have the following version of first-order Peano axioms:


*

*$\forall x\left[\neg0=s(x)\right]$

*$\forall x\forall y\left[x=y\leftrightarrow s(x)=s(y)\right]$

*$\forall\overline{y}\left[F(0,\overline{y})\wedge\forall x\left[F(x,\overline{y})\rightarrow F\left(s(x),\overline{y}\right)\right]\rightarrow\forall zF(z,\overline{y})\right]$, where $F$ is any formula of $k+1$ variables and $\overline{y}=y_{1},y_{2},...,y_{k}$.
From them it follows that everything is in $\mathbb{N}$ (thus, $\left|D\right|=\aleph_{0}$). Then, I can not see how we get to the conclusion.
 A: You give a second order axiomatizaton of $(\mathbb N, s)$, which is enough to characterize $(\mathbb N,s)$ up to isomorphism. But $\operatorname{Th}(\mathbb N,s)$ does not (usually) denote its consequences... it denotes the set of all of the first-order sentences true in $(\mathbb N,s).$ Furthermore, the core question is about first-order definability, so second order logic is irrelevant. (But to clarify, I'll note that $\mathbb N+\mathbb Z+\mathbb Z$ is not a model of the second order theory... as I mentioned, the only model of this is $\mathbb N.$)
You are right about what $\mathbb N+\mathbb Z+\mathbb Z$ means. You can think of the + as disjoint union, and then the successor operation behaves "locally" like you expect it to.
Let's clarify what first-order definability of $\le$ in $(\mathbb N,s)$ means. It means there is a first-order formula $\varphi(x,y)$ in the language with a single non-logical unary function symbol $s$ such that for any $n,m\in \mathbb N,$ $$\left((\mathbb N,s)\models \varphi(n,m)\right)\iff n\le m.$$ Because $\le$ is a linear order, $\varphi$ satisfies all of the axioms for a linear order (which are all first order). For instance, $$ (\mathbb N,s)\models \forall x,y,z((\varphi(x,y)\land \varphi(y,z))\to \varphi(x,z))$$ (which is the transitivity axiom). Thus since all the sentences that say $\varphi$ defines a linear order are first order sentences true in $(\mathbb N,s),$ they are consequences of $\operatorname{Th}(\mathbb N,s),$ which recall is just consists of all first order sentences true in $(\mathbb N,s).$ Therefore, if $\varphi$ defines $\le$ (or any linear order) in $(\mathbb N,s),$ it will define a linear order in any model of $\operatorname{Th}(\mathbb N,s).$
So now we are done if we can show that there are models of $\operatorname{Th}(\mathbb N, s)$ with no definable linear ordering. It is not trivial that $\mathbb N+\mathbb Z+\mathbb Z$ is a model of $\operatorname{Th}(\mathbb N,s),$ (i.e. it satisfies all the same first order sentences as $\mathbb N$ in the language with just $s$) but proving that here would take too much space, so we'll take it for granted. Now, as Noah's answer says, if $a$ is in one copy of $\mathbb Z$ and $b$ is in the other, then there is an automorphism $\sigma$ of $(\mathbb N+\mathbb Z+\mathbb Z,s)$ such that $\sigma(a)=b$ and $\sigma(b)=a.$ We simply leave the copy of $\mathbb N$ alone and switch $a$ and $b,$ and take $a$ and $b$'s successors and predecessors along for the ride. (So $\sigma(s(a))$ = $s(b),$ etc.)
But this means that no definable ordering can exist. Let $\varphi(x,y)$ define some ordering $\le$ on $\mathbb N+\mathbb Z+\mathbb Z$ (nevermind if it agrees with the standard ordering when restricted on $\mathbb N$... we're showing something stronger). Let $a$ and $b$ be as above. If $a\le b$ then $$(\mathbb N+\mathbb Z+\mathbb Z,s)\models \varphi(a,b),$$ but since $\sigma$ is an automorphism, $$(\mathbb N+\mathbb Z+\mathbb Z,s)\models \varphi(\sigma(a),\sigma(b))\implies (\mathbb N+\mathbb Z+\mathbb Z,s)\models \varphi(b,a)\implies b\le a.$$ But this conflicts with the fact that $\le$ is antisymmetric: if $a\ne b$ and $a\le b$ then $b\not\le a.$
So that's it.

Finally, I'll add a note on your last paragraph that I mentioned in the comments: it is (almost) never the case that a collection of first order axioms will have only one possible cardinality for its models, much less have only one model up to isomorphism. This is a consequence of the compactness theorem / upward Lowenheim-Skolem theorem. This situation is no exception: $\mathbb N$ with any uncountable number of copies of $\mathbb Z$ is a model of $\operatorname{Th}(\mathbb N).$ 
It is also a model of the effective first order theory you wrote down. It is true that the theory you wrote down has the exact same consequences as $\operatorname{Th}(\mathbb N,s),$ but this is only the case since it happens to be complete. If we were instead comparing $\operatorname{Th}(\mathbb N, s,+,\cdot,0,1,\le)$ with the full first order PA, then these aren't the same thing, since PA is (famously) incomplete. $\operatorname{Th}(\mathbb N,s, +,\cdot,0,1,\le)$ is all the true first order sentences, and only some of these are consequences of PA. 
