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.
$\begingroup$
$\endgroup$
7
-
3$\begingroup$ "ordered abelian groups" is not a class of abelian groups, it's an additional structure. If one only assumes the existence of such a structure without fixing it, one gets orderable abelian groups, which are precisely torsion-free abelian groups. $\endgroup$– YCorCommented Aug 19, 2021 at 21:45
-
$\begingroup$ @Ycor yes this is correct, but at least we know that in such a group, every formula $\varphi(\overline{x})$ (in the language of groups)is equivalent to a quantifier-free formula $\psi(\overline{x})$ (possibly containing $<$) and this is also good. $\endgroup$– Sh.M1972Commented Aug 20, 2021 at 3:19
-
2$\begingroup$ @EmilJeřábek Any ordered abelian group with quantifier elimination in the language of ordered abelian groups is divisible. Proof: It's easy to see that QE implies o-minimality, and it is well known and easy to see that o-minimality implies divisibility. $\endgroup$– Erik WalsbergCommented Aug 23, 2021 at 22:19
-
2$\begingroup$ A lot more oag's have qe if you add predicates defines the set of nth multiples for all n, for example any archimedean ordered abelian group has QE in this language. $\endgroup$– Erik WalsbergCommented Aug 23, 2021 at 22:23
-
2$\begingroup$ There is also a description of definable sets in arbitrary oag's, see the paper "Quantifier elimination in ordered abelian groups". You can eliminate quantifiers down to very special kinds of quantifiers that take some work to define. $\endgroup$– Erik WalsbergCommented Aug 24, 2021 at 4:58
|
Show 2 more comments
1 Answer
$\begingroup$
$\endgroup$
8
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$.) This result for abelian groups is originally due to Szmielew.
answered Aug 19, 2021 at 21:20
-
$\begingroup$ Does this mean that if one defines, in an abelian group $A$, $F_n(x)$ as the formula expressing $x\in nA$, one gets quantifier elimination after adding each $F_n$ ($n$ positive integer) to the language? $\endgroup$– YCorCommented Aug 19, 2021 at 21:49
-
1$\begingroup$ @YCor I believe that's correct. I learned this from Alex Kruckman. $\endgroup$ Commented Aug 19, 2021 at 21:56
-
$\begingroup$ @TimCampion thanks for pointing out this very detailed post! $\endgroup$– YCorCommented Aug 19, 2021 at 21:58
-
1$\begingroup$ @Sh.M1972 Yes, there are no further parameters. $\endgroup$ Commented Aug 20, 2021 at 7:54
-
1$\begingroup$ @YCor Yes, but I stress that that will be quantifier elimination in $A$ (i.e., in the theory $\mathrm{Th}(A)$), not in the theory of all abelian groups. $\endgroup$ Commented Aug 20, 2021 at 7:58