Presburger arithmetic with unary predicates is Π11 complete
Joseph Yehuda Halpern · Journal of Symbolic Logic · 1991
Abstract We give a simple proof characterizing the complexity of Presburger arithmetic augmented with additional predicates. We show that Presburger arithmetic with additional predicates is complete. Adding one unary predicate is enough to get hardness, while adding more predicates (of any arity) does not make the complexity any worse.