On the complexity of quantified linear systems

In this paper, we explore the computational complexity of the conjunctive fragment of the first-order theory of linear arithmetic. Quantified propositional formulas of linear inequalities with (k − 1) quantifier alternations are log-space complete in ΣPk or ΠPk depending on the initial quan-tifier. We show that when we restrict ourselves to quantified conjunctions of linear inequali-ties, i.e., quantified linear systems, the complexity classes collapse to polynomial time. In other words, the presence of universal quantifiers does not alter the complexity of the linear program-ming problem, which is known to be in P. Our result reinforces the importance of sentence formats from the perspective of computational complexity