Quantifier elimination for modules with scalar variables (Q1192337)

The Baur-Monk theorem [\textit{W. Baur}, Isr. J. Math. 25, 64-70 (1976; Zbl 0354.02043)] states that for any fixed ring \(R\) the theory of \(R\)-modules admits elimination of quantifiers up to positive primitive formulas and invariant statements. This paper shows that actually one can get a much more general result, namely that in the two-sorted theory of modules over a ring (one sort for the ring and one for the module) one can, for formulas in which all scalar (i.e. ring) variables are free, eliminate quantifiers up to two-sorted positive primitive formulas and two-sorted invariant statements. Here a two-sorted positive primitive formula and a two-sorted invariant statement are as usual only that ring elements are now replaced by terms of the ring sort. Furthermore the authors show that in the case of the two-sorted theory of torsion-free modules over Bezout domains (those integral domains in which each finitely generated ideal is principal) one can in the above elimination of quantifiers replace the two-sorted positive primitive formulas and two-sorted invariant statements by more explicit formulas in a language naturally associated with these structures. Finally, as a consequence of their work, the authors show that in the case of the two-sorted theory of the integers as a module over itself, the set \(\{(\bar r,\bar x);\varphi(\bar r,\bar x)\text{ holds}\}\) is polynomial-time decidable for any two-sorted formula \(\varphi(\bar r,\bar x)\) without quantified scalar variables.