Quantifier elimination for abelian groups In the Wikipedia article  (https://en.wikipedia.org/wiki/Quantifier_elimination#cite_note-4) it is said that every abelian group has quantifier elimination property and a long old paper of W. Szmielew (1955) is given as a reference. But as far as I know, this is true for special classes of abelian groups (like divisible, ordered, ... groups). I am not an expert of model theory but I need to apply quantifier elimination for  reduced abelian groups (abelian groups the only divisible subgroup in which is the trivial one), so I need to know if really we have quantifier elimination for any abelain group and if not, what is the most complex quantifier combination of formulas in such groups.
 A: Abelian groups are the same thing as $\mathbb Z$-modules. In general, for any ring $R$, the theory of left $R$-modules has quantifier elimination down to Boolean combinations of primitive positive formulas and certain sentences (expressing so-called Baur–Monk invariants). This is the Baur–Monk quantifier elimination theorem; see e.g. §A.1 in Hodges, Model Theory.
In particular, since the theory of any particular abelian group or $R$-module is complete, it has quantifier elimination down to Boolean combinations of p.p. formulas.
Note that a p.p. formula expresses solvability of a linear system; in the case where $R$ is a PID (including abelian groups with $R=\mathbb Z$), the Smith normal form shows that you can reduce to the case of p.p. formulas with one quantifier. That is, every formula $\phi(\vec x)$ is equivalent to a Boolean combination of invariant sentences and the divisibility formulas $a\mid\sum_ia_ix_i$ for some $a,a_i\in R$. (For $a=0$, this amounts to the original atomic formulas $\sum_ia_ix_i=0$.)
