The decision complexity of Presburger PA and its variants has received much attention in the literature. We investigate the complexity of quantifier elimination procedures for PA - a topic that is even more relevant for applications. First we show that the author's triply exponential upper bound is essentially tight. This fact seems to preclude practical applications. By weakening the concept of quantifier elimination slightly to bounded quantifier elimination, we show, however, that the upper and lower bound for quantifier elimination in PA can be lowered by exactly one exponential. Moreover we gain uniformity in the coefficients, a property that we prove to be impossible for complete quantifier elimination in PA. Thus we have tight upper and lower complexity bounds for elimination theory in PA and uniform PA. The results are inspired by experimental implementations of bounded quantifier elimination that have solved non-trivial application problems e.g. in parametric integer programming.
Ulrike Peiker, Martin Griebl