Theory of torsion-free divisible Abelian groups allowing the trivial group (source code)

= Theory of torsion-free divisible Abelian groups allowing the trivial group
{title2=$\mathrm{DAG}^{\prime}$}

= DAG prime
{c}
{synonym}

Remove the nonzero-model axiom from <DAG>. The inclusion $\{0\}\subseteq\mathbb Q$ is then an inclusion of models but is not a <simple closure>, because $x\ne0$ has a witness only in the larger model. The theory does not have <quantifier elimination>: all closed group terms are zero, so no quantifier-free sentence distinguishes the two models.