Bounding Variables in Presburger Arithmetic

We can use insights from quantifier elimination to obtain alternative algorithms for deciding formulas.

Define $exp_0(n)=n$ and $exp_{k+1}(n)=2^{exp_k(n)}$ for all $k \ge 0$ .

Bounds Showing Membership in 2EXPSPACE

Let $s(F)$ denote the maximum of the constant $2$ and of all constants ocurruring in the formula $F$ .

Theorem (Oppen): There exists a constant $e$ such that the following is true. If $F$ is a formula of Presburger arithmetic with $n$ quantifiers, then when Cooper's procedure is applied to $F$ , every integer constant encountered is bounded by

$\begin{equation*} s(F)^{exp_2(en)} \end{equation*}$

Lemma (Ferrante, Rackhoff): There exists a constant $g$ such that the following is true. Let $B$ be the formula $Q_1 x_1 \ldots Q_nx_nF(x_1,\ldots,x_n)$ , where $F$ is quantifier-free and $Q_i$ is $\forall$ or $\exists$ for each $i$ , $1 \le i \le n$ , and let $s_0 = s(F)$ . Then $B$ is true iff

$\begin{equation*} (Q_1 x_1 \preceq s_0^{exp_2(gn+1)}) \ldots (Q_n x_n \preceq s_0^{exp_2(gn+n)}) F(x_1,\ldots,x_n) \end{equation*}$

where $a \preceq b$ means $|a| \le b$ .

Bounded Quantifier Alternation

Example: if $F$ has no quantifiers, then these two formulas have one quantifier alternation:

$\begin{equation*} \forall x_1.\forall x_2. \forall x_3. \exists y_1. \exists y_2. \exists y_3. \exists y_4. F \end{equation*}$

$\begin{equation*} \exists u_1.\exists u_2. \exists u_3. \forall v_1. \forall v_2. \forall v_3. F \end{equation*}$

and this formula has two quantifier alternations:

$\begin{equation*} \forall x. \exists y. \forall z. F \end{equation*}$

Definition: A formula in prenex form has $m-1$ quantifier alternations iff it is the form

$\begin{equation*} ((Q_{11} x_{11}) \ldots (Q_{1n_1} x_{1n_1})) \ldots ((Q_{m1} x_{m1}) \ldots (Q_{mn_n} x_{mn_m})).\ F \end{equation*}$

where for the same $i$ , all quantifiers $j$ $Q_{ij}$ are the same type (either all are $\exists$ or all are $\forall$ ), and for $i$ and $i+1$ the quantifiers are of different type.

Theorem (Reddy, Loveland, 1978): If $F$ is a closed Presburger arithmetic formula $(Q_1 x_1) \ldots (Q_r x_r) G(x_1,\ldots,x_r)$ of size $n>4$ with $m$ quantifier alternations, where $Q_1,\ldots,Q_r$ are quantifiers and $G$ is quantifier-free, then $F$ is true iff the formula

$\begin{equation*} \left(Q_1 x_1 \leq exp_2((c+1)n^{m+3})\right) \ldots \left(Q_r x_r \leq exp_2((c+r)n^{m+3})\right) G(x_1,\ldots,x_r) \end{equation*}$

with bounded quantifiers is true for some $c > 0$ .

In general, it is often quantifier alternations that cause high complexity of the decision procedure, not quantifiers themselves.

References

Reddy, Loveland: Presburger Arithmetic with Bounded Quantifier Alternation, pdf
Lararuk, Sturm: Weak quantifier elimination for the full linear theory of the integers, pdf

Ferrante, Rackoff: A Decision Procedure for the First-Order Theory of Addition with Order, pdf (NOTE: this is for real numbers, not integers)