I want to prove that the structure $(\Bbb{Q},+,0)$ has Quantifier Elimination. I can prove it for some simple basic formulas, but what if i get a formula which says that i have a linear combination, for example:
$\exists x [x_i+x_j=x+x_k+x_l \wedge\rho]$
with $x_i,x_j$, etc. free variables and $\rho$ the rest of the formula. My problem is that we can not substitute $x$ by something as in the case $\exists x[x=x_j\wedge\rho]$, because here we can sustitute $x$ by $x_j$ in the formula $\rho$. If someone has an idea?! This would be very good :) Thank you :) PS. I hope thats a good idea to prove QE of the structure ;)
Isn't Quantifier Elimination a property of a theory? It seems like you have a model of a particular theory, so it doesn't make sense to talk about a particular model having quantifier elimination. In any case, if you are looking at the theory of torsion free divisible abelian groups, then that theory does admit QE and your mode structure is a model of that theory.
A good approach to proving QE, is to look at 2 models, $M,N$ of the theory which have a common substructure A. If you have a $L_A$ formula $p(y)$ which is a conjunction of atomic literals in one variable, then if $p(y)$ has a realization in $M$ implies that it has a realization in $N$, then your theory has QE. This approach works for showing that DAG admits QE. Check out David Marker's book: Model Theory an Introduction.