# Theory of (Q,+,0) has QE

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?

-
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