Characterizing $(\mathbb{Z}, <)$ up to isomorphism

Question

Is there an (obvious) way to characterize the structure $(\mathbb{Z}, <)$ up to isomorphism (where $<$ is the usual total ordering on the integers) by a sentence of infinitary first-order logic (i.e. first-order logic with infinite disjunctions and conjunctions)? In particular, the characterizing sentence must be a sentence of the vocabulary with only one binary relation symbol.

Answer 1

Sure: $(\mathbb{Z},<)$ is the unique non-empty discrete linear order without endpoints such that for any two elements, there are finitely many elements between them.

So that's the conjunction of the following sentences of $\mathcal{L}_{\omega_1,\omega}$:

\begin{gather*} \exists x\, (x=x)\\ \forall x\, \lnot (x < x)\\ \forall x\,\forall y\, \forall z\, ((x < y\land y < z)\rightarrow x < z)\\ \forall x\, \forall y\, (x < y \lor y < x \lor x = y)\\ \forall x\, \exists y\, (x < y \land \lnot \exists z\,(x < z \land z < y))\\ \forall x\, \exists y\, (y < x \land \lnot \exists z\,(y < z \land z < x)\\ \forall x\, \forall y\, (x < y \rightarrow \bigvee_{n\in \omega} (\exists z_1\dots \exists z_n \forall w ((x < w \land w < y)\rightarrow \bigvee_{i=1}^n (w = z_i)))) \end{gather*}

$\exists x\, (x=x)$ is not necessary if your convention is that all structures are non-empty.

To see that this characterizes $(\mathbb{Z},<)$ up to isomorphism, let $M$ be any model. Pick any element $a_0\in M$, since $M$ is non-empty. By induction, define $a_{n+1}$ to be the (unique) successor of $a_n$, and define $a_{-(n+1)}$ to be the (unique) predecessor of $a_{-n}$. For any $b\in M$, if there are $k$ elements between $a_0$ and $b$, then $b = a_{k+1}$ if $a_0 < b$ or $b = a_{-(k+1)}$ if $b < a$. So every element of $M$ is $a_n$ for some $n$. Then $n\mapsto a_n$ is an isomorphism $\mathbb{Z}\cong M$.