Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
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 $\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.
A bit belatedly, here's another approach:
The presence of constant symbols naming each element of the structure in question does not entirely prevent an automorphism-based argument from working. We just have to pass to a different structure!
By compactness + downward Lowenheim-Skolem, our original structure $\mathcal{Q}$ has a countable non-Archimedean elementary extension $\mathcal{X}$. By a back-and-forth argument, the substructure of $\mathcal{X}$ consisting of the positive infinite elements is a single automorphism orbit, and so any (parameter-freely-)${}$definable-in-$\mathcal{X}$ set contains either all or none of the infinite elements of $\mathcal{X}$.
Now supposing $\varphi$ defines $\mathbb{Z}$ in $\mathcal{Q}$, consider $\varphi^\mathcal{X}$ and apply elementarity to the property "is unbounded and co-unbounded."
