= 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.
Back to article page
