Paper detail

Subclasses of Presburger Arithmetic and the Weak EXP Hierarchy

It is shown that for any fixed $i>0$, the $Σ_{i+1}$-fragment of Presburger arithmetic, i.e., its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\mathsfΣ^{\mathsf{EXP}}_{i}$, 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 $Σ_1$-fragment of Presburger arithmetic: given a $Σ_1$-formula $Φ(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.