Subclasses of Presburger arithmetic and the polynomial-time hierarchy (Q1115858)

The author investigates the complexity of subclasses of Presburger arithmetic (PA). He shows that if a formula \(G=Q_ 1x_ 1Q_ 2x_ 2...Q_ sx_ sF(x_ 1,x_ 2,...,x_ s)\) (with quantifier-free F) of length n has m quantifier alternations, then G is true in PA if and only if the formula G', obtained from G by means of replacing all the quantifiers \(Q_ ix_ i\) by the bounded ones \(Q_ i(x_ i\leq w)\), where \(w=2^{cn^{(s+3)^{n+2}}}\), is true in PA. For arbitrary quantifiers prefix \(Q_ 1Q_ 2...Q_ s\) with m alternations, if \(Q_ 1=\exists\) \((Q_ 1=\forall)\) then every sentence \(Q_ 1x_ 1Q_ 2x_ 2...Q_ sx_ sF\) (with quantifier-free F) which is true in PA belongs to \(\Sigma^ p_{m-1}\) (respectively, \(\Pi^ p_{m-1})\). The set of PA-true sentences with prefix \(\exists \forall \exists\) is NP-complete. Parallel results are obtained for formulas with quantifier prefix of the types \(\exists_ 1\forall_ 2...\exists_ m\exists^ 2\forall^ 3\) and \(\exists_ 1\forall_ 2...\forall_ m\forall^ 2\exists^ 3\). Finally, the author shows that for all polynomials p there exist formulas \(\exists yH(x_ 1x_ 2x_ 3y)\) with no equivalent formulas \(\tilde H(x_ 1,x_ 2,x_ 3)\) of length \(| \tilde H| \leq p(| H|)\) where H, \(\tilde H\) are quantifier-free.