Quantifier Elimination I want to prove the following: The structure $(\mathbb{Z},\equiv,0)$ has QE (with $\equiv$ a relation  such that for all $m,n\in\mathbb{Z}$: $m\equiv n$ iff $m-n$ is even). I thought hereover in the following way: Suppose you have a formula $\phi$ in the language of the structure. Then bring this formula to the disjunctive normal form. The basis formulas in the language are: $$a=b,\neg(a=b),a=0,\neg(a=0),(a\equiv b),\neg(a\equiv b),(a\equiv 0),\neg(a\equiv 0)$$
and also combinations with $\wedge$. But than i have to find for all possible combinations a quantifier free formula. But how to do this? 
Wat shall I do if i want to prove that a given structure has no QE?
Thank you ;)
 A: *

*First, notice that $a\equiv b$ is equivalent to $(a\equiv 0\wedge b\equiv 0)\vee (a\not\equiv 0\wedge b\not\equiv 0)$, and similarly for $a\not\equiv b$, so you can assume that there are none of those at the very beginning (before taking the normal form).

*If you have a formula of the form $\varphi=\exists x \varphi'(x,\overline y)$ with $\varphi$ a conjunction of literals, one of which is $x=y_j$, then $\varphi$ is equivalent to $\varphi'(y_j,\overline y)$.

*All other $\varphi$ are necessarily contradictory or tautological, which I will leave to you to prove.


Quantifier elimination is equivalent to substructural completeness, that is, a theory $T$ has q.e. iff for any model $M\models T$ and a nonempty subset $A$ of its universe, $T$ with the atomic diagram of $A$ is complete (or, equivalently, that any two models containing $A$ are elementarily equivalent), so you can show that a theory doesn't have q.e. by exhibiting a counterexample to substructural completeness (which may still be quite hard, as you need to find a suitable $A$ and show that some theory is not complete).


*

*For example, the theory of abelian groups does not have q.e., because any set of integers can be extended to, among others, the integers themselves, or the rationals, but the two are not elementarily equivalent.

*For a complete (and model complete!) example, the theory of real closed fields (in the language $\{0,1,+,\cdot\}$) does not have q.e., because if we take some two algebraically independent real numbers $a,b$, then their atomic diagram will always be the same, but one is bigger than the other ($(\exists x) a+x^2=b$ or $(\exists x) b+x^2=a$), so we can't decide which.

