Dgdrxrt

With $Q$ the set of rational numbers, I'm wondering:

Is the predicate "Int($x$) $equiv$ $x$ is an integer" first-order definable in $(Q, +, <)$ where there is one additional constant symbol for each element of $Q$?

I know this is the case if multiplication is allowed. I guess the fact that $<$ is dense would imply a negative answer to this question, via an EF game maybe; is there a similar structure with a dense order but with Int($x$) FO-definable?

This is a very interesting question.

The answer is no.

First, I claim that the theory of the structure $langlemathbbQ,+,ltrangle$ 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 xvarphi(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(ult v)$ is equivalent to $vlt uvee 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+ylt 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 $acdot xneq t$, or that $bcdot xlt s$ or that $ult ccdot 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 $frac1cu$ 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.