Exists first-order formula $Z(x)$ in language $\langle 0, +, \le\rangle$ that over field $\mathbb{Q}$ expresses fact that $x$ is integer? This is a followup to my previous questions here and here.
Does there exist any first-order formula $Z(x)$ in the language $\langle 0, +, \le\rangle$ that over the field $\mathbb{Q}$ of rational numbers expresses the fact that $x$ is an integer?
I strongly suspect there isn't any, but I don't know how to see that. Could anybody help?
 A: You are correct: no such formula exists.
Suppose that $Z(x)$ is such a formula. That is, for each $q \in \mathbb{Q}$
$$\mathfrak{Q} = \langle \mathbb{Q}, 0 , + , \leq \rangle \models Z[q] \Leftrightarrow q \in \mathbb{Z}. \tag{1}$$
Note that the mapping $\sigma (x) = \frac{x}{2}$ is an isomorphism of $\mathfrak{Q}$, and so for each $q \in \mathbb{Q}$ we have that $$\mathfrak{Q} \models Z[q] \Leftrightarrow \mathfrak{Q} \models Z[ \sigma(q) ]. \tag{2}$$
Now consider what happens when $q = 1$: By (2) we have that
$$\mathfrak{Q} \models Z[1] \Leftrightarrow \mathfrak{Q} \models Z[\sigma(1) = \tfrac{1}{2}],$$ which clearly contradicts our assumption (1).
A: While @komorebi's answer is correct, approaching this question using automorphisms is a bit fragile. In particular, the automorphism method cannot rule out the possibility that the integers are definable with parameters (that is, after adding some constants). To see why, observe that there are no non-trivial automorphisms fixing a non-zero number.
Fortunately, there is classification of all definable sets in this structure: a subset of $\mathbb{Q}^n$ is definable (possibly with parameters) in the language $(\mathbb{Q},+,<)$ if and only if it is a Boolean combination of solution sets to linear inequalities. In particular, a subset of $\mathbb{Q}$ is definable (with parameters) if and only if it is a Boolean combination of intervals and points, so $\mathbb{Z}$ is not definable.
The above result is a consequence of quantifier elimination for the theory of divisible ordered Abelian groups. (Really, it's just a restatement of that fact.) That fact, in turn, is an approachable exercise: prove by induction on formulas that every formula in the language $(+,<)$ is equivalent (modulo the theory of divisible ordered Abelian groups) to a quantifier free formula.
