hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO
Abstract:
The first-order theory of addition over the natural numbers, known as
Presburger arithmetic, is decidable in double exponential time. Adding an
uninterpreted unary predicate to the language leads to an undecidable theory.
We sharpen the known boundary between decidable and undecidable in that we show
that the purely universal fragment of the extended theory is already
undecidable. Our proof is based on a reduction of the halting problem for
two-counter machines to unsatisfiability of sentences in the extended language
of Presburger arithmetic that does not use existential quantification. On the
other hand, we argue that a single $\forall\exists$ quantifier alternation
turns the set of satisfiable sentences of the extended language into a
$\Sigma^1_1$-complete set. Some of the mentioned results can be transfered to
the realm of linear arithmetic over the ordered real numbers. This concerns the
undecidability of the purely universal fragment and the $\Sigma^1_1$-hardness
for sentences with at least one quantifier alternation. Finally, we discuss the
relevance of our results to verification. In particular, we derive
undecidability results for quantified fragments of separation logic, the theory
of arrays, and combinations of the theory of equality over uninterpreted
functions with restricted forms of integer arithmetic. In certain cases our
results even imply the absence of sound and complete deductive calculi.
