Bounding quantification in parametric expansions of Presburger arithmetic

Abstract

Generalizing Cooper’s method of quantifier elimination for Presburger arithmetic, we give a new proof that all parametric Presburger families $\{S_t : t \in \mathbb {N}\}$ [as defined by Woods (Electron J Comb 21:P21, 2014)] are definable by formulas with polynomially bounded quantifiers in an expanded language with predicates for divisibility by f(t) for every polynomial $f \in \mathbb {Z}[t]$. In fact, this quantifier bounding method works more generally in expansions of Presburger arithmetic by multiplication by scalars $\{\alpha (t): \alpha \in R, t \in X\}$ where R is any ring of functions from X into $\mathbb {Z}$.