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

I want to prove that $Th(\mathbb{Q},+,0)$ has quantifier elimination. Please point out where i go wrong or how to finish my reasoning:

We can bring the formula in disjunctive normal form and distribute the existential quantifier. So we are left with a conjunction of literals. Now the basic formula's can be brought to 'additive normal form' (I don't know if this is usual terminology), so $m_0 x_0 + ... + m_{n-1} x_{n-1} + m x = 0$ or an inequality, where $x$ is the variable from the existential quantifier.

But then?

share|cite|improve this question
Sketch: assume the coefficient of $x$ in the basic formulas are non-zero. If some formula is an equality, you can solve for $x$ (in terms of the other variables) and substitute. If all the formulas are disequalities, they can always be satisfied (by choosing a sufficiently large $x$). – Colin McQuillan Jan 30 '13 at 12:17

Your Answer


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

Browse other questions tagged or ask your own question.