 Quantifier elimination for torsion-free divisible Abelian groups

In a torsion-free divisible Abelian group, division by a nonzero integer is unique. The rational scalar operations are therefore a definitional expansion. Formulas reduce to Boolean combinations of rational linear equations: eliminate an existential variable in a conjunction by solving any equation with nonzero coefficient; if none fixes the variable, the finitely many nontrivial disequalities exclude only finitely many choices in an infinite group. Equations with zero coefficient reduce to parameter conditions.

Thus over a finite parameter set a complete one-variable type either specifies an element of its linear span, or excludes every element of that span. An uncountable rational vector space realizes the latter type because a finite-parameter span is countable. It is consequently an omega-saturated model in the additive language.