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?

  • 1
    $\begingroup$ I don't see how Int is definable even when multiplication is allowed. Do you have a source ? $\endgroup$
    – mercio
    May 22 '11 at 6:56
  • 5
    $\begingroup$ @chandok: this is a famous result of Julia Robinson. JSTOR link $\endgroup$ May 22 '11 at 7:08

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.

  • $\begingroup$ Thank you very much. This indeed answers my question. I later found a reference which answered this question in a similar way (van Den Dries book on O-minimal structures) but I'd love to see a logic oriented book on the matter; would you know one by any chance? $\endgroup$ May 23 '11 at 17:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.