Quantifier elimination for modules with scalar variables
type: Item
instance of: scholarly article
title: Quantifier elimination for modules with scalar variables
zbMATH Open document ID: 0772.03017
DOI: 10.1016/0168-0072(92)90025-U
published in: Annals of Pure and Applied Logic
publication date: 1992-09-27T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03C60
Mathematics Subject Classification ID: 03C10
Mathematics Subject Classification ID: 13L05
zbMATH DE Number: 60740
zbMATH Keywords: two-sorted modules
zbMATH Keywords: Presburger arithmetic
zbMATH Keywords: two-sorted theory of modules over a ring
zbMATH Keywords: two-sorted positive primitive formulas
zbMATH Keywords: two-sorted invariant statements
zbMATH Keywords: torsion-free modules
zbMATH Keywords: Bezout domains
zbMATH Keywords: integral domains
author: Lou van den Dries
author: Jan E. Holly
reviewed by: Roger Villemaire
MaRDI profile type: Publication
cites work: Elimination of quantifiers for modules
cites work: Integer Programming with a Fixed Number of Variables
cites work: Q4039792
cites work: Model theory of modules
full work available at URL: 0168-0072(92)90025-u
OpenAlex ID: W1987803410
Recommended article: Decidability and modules over Bézout domains
Recommended article: Q3128008
Recommended article: The model completion of the theory of modules over finitely generated commutative algebras
Recommended article: On the decidability of the theory of modules over the ring of algebraic integers
Recommended article: A Formal Quantifier Elimination for Algebraically Closed Fields
Recommended article: Q4517146
Recommended article: Q4944919
Recommended article: ELIMINATION OF QUANTIFIERS OVER VECTORS IN SOME THEORIES OF VECTOR SPACES
Recommended article: Decidability for Theories of Modules
Recommended article: THE STRUCTURE OF MODELS AND A DECIDABILITY CRITERION FOR COMPLETE THEORIES OF FINITE-DIMENSIONAL ALGEBRAS
description: scientific article; zbMATH DE number 60740