Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy

Abstract

It is shown that for any fixed $i>0$, the ${\Sigma }_{i+1}$-fragment of Presburger arithmetic, i.e., its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for ${\mathsf{\Sigma }}_i^{\mathsf{EXP}}$, the $i$-th level of the weak EXP hierarchy, an analogue to the polynomial-time hierarchy residing between $\mathsf{NEXP}$ and $\mathsf{EXPSPACE}$. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer & Rabin in 1974. Moreover, we apply some of the techniques developed in the proof of the lower bound in order to establish bounds on sets of naturals definable in the ${\Sigma }_1$-fragment of Presburger arithmetic: given a ${\Sigma }_1$-formula $\Phi (x)$, it is shown that the set of non-negative solutions is an ultimately periodic set whose period is at most doubly-exponential and that this bound is tight.

10 pages, 2 figures

Cited by in corpus (2)

• Integer Vector Addition Systems with States
• On Presburger arithmetic extended with non-unary counting quantifiers