Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 in 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?

share|cite|improve this question
I don't see how Int is definable even when multiplication is allowed. Do you have a source ? – mercio May 22 '11 at 6:56
@chandok: this is a famous result of Julia Robinson. JSTOR link – Chris Eagle May 22 '11 at 7:08
up vote 15 down vote accepted

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.

share|cite|improve this answer
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? – Michaël Cadilhac May 23 '11 at 17:18

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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