FO-definability of the integers in (Q, +, <)

Solution 1:

This is a very interesting question.

The answer is no.

First, I claim that the theory of the structure $\langle\mathbb{Q},+,\lt\rangle$ admits elimination of quantifiers. That is, every formula $\varphi(\vec x)$ in this language is equivalent over this theory to a quantifier-free formula. This can be proved by a brute-force hands-on induction over formulas. Allow me merely to sketch the argument. It is true already for the atomic formulas, and the property of being equivalent to a quantifier-free formulas is preserved by Boolean connectives. So consider a formula of the form $\exists x\varphi(x,\vec z)$, where $\varphi$ is quantifier-free. We may put $\varphi$ in disjunctive normal form and then distribute the quantifier over the disjunct, which reduces to the case where $\varphi$ is a conjunction of atomic and negated atomic formulas. We may assume that $x$ appears freely in each of these conjuncts (since otherwise we may remove it from the scope of the quantifier). If a formula of the form $x+y=z$ appears in $\varphi$, then we may replace all occurences of $x$ with $z-y$ and thereby eliminate the need to quantify over $x$ (one must also subsequently eliminate the minus sign after the replacing, but this is easy by elementary algebraic operations). We may do this even if $x$ appears multiply, as in $x+x+y=z$, for then we replace $x$ everywhere with $(z-y)/2$, but then clear both the $2$ and the minus sign by elementary algebraic manipulations. Thus, we may assume that equality atomic assertions appear only negatively in $\varphi$. All the other assertions merely concern the order. Note that a negated order relation $\neg(u\lt v)$ is equivalent to $v\lt u\vee v=u$, and we may distribute the quantifier again over this disjunct. So negated order relations do not appear in $\varphi$. The atomic order formulas have the form $x+y\lt u+v$ and so on. We may cancel similar variables on each side, and so $x$ appears on only one side. By allowing minus, we see that every conjunct formula in $\varphi$ says either that $a\cdot x\neq t$, or that $b\cdot x\lt s$ or that $u\lt c\cdot x$, for some terms $t,s,u$, in which $+$ and $-$ may both appear, and where $a$, $b$ and $c$ are fixed positive integer constants. By temporarily allowing rational constant coefficients, we may move these coefficients to the other side away from $x$. Thus, the assertion $\exists x\,\varphi(x,\vec t,\vec s,\vec u)$ is equivalent to the assertion that every $\frac{1}{c}u$ is less than every $\frac 1b s$. We may then clear the introduced rational constant multiples by multiplying through (which means adding that many times on the other side). Clearly, if such an $x$ exists, then this will be the case, and if this is the case, then there will be $x$'s in between, and so infinitely many, so at least one of them will be unequal to the $t$'s. This final assertion can be re-expressed without minus, and so the original assertion is equivalent to a quantifier-free assertion. So the theory admits elimination of quantifiers.

It now follows that the definable classes are all defined by quantifier-free formulas. By induction, it is easy to see that any such class will be a finite union of intervals, and so the class of integers is not definable.