April 2022 – Thinking

Every once in a while I start modelling a problem using a logical formalism and need to remind myself of the decidability of various first-order theories and the complexity results for those that are decidable. Inevitably, I end up spending a long time looking back over literature I once read, with results sprinkled in different places.

This post summarises some of this information in one place for me or others to find in the future, with a skew towards those theories of interest for arithmetic. The information here is primarily taken from Bradley and Manna supplemented with various other sources linked. The usual definitions of $\Omega$ and $O$ are used.

Theory	Description	Full theory	Quantifier-free conjunctive fragment	Quantifier elimination algorithm
$T_{\mathrm{E}}$ (see note 1)	Equality	Undecidable	$O(n \log n)$ (Downey et al.) Congruence closure algorithm	N/A
$T_{\mathrm{PA}}$	Peano arithmetic	Undecidable	Undecidable	N/A
$T_{\mathbb{N}}$	Presburger arithmetic	$\Omega\left(2^{2^n}\right)$ (Fischer and Rabin) $O\left(2^{2^{2^{kn}}}\right)$ (Oppen)	NP-complete (Scarpellini)	Cooper’s Algorith m (see note 2)
$T_{\mathbb{R}}$ (see note 3)	Real arithmetic (with multiplication)	$O\left(2^{2^{kn}}\right)$	$O\left(2^{2^{kn}}\right)$	Collins’ Cylindrical Algebraic Decomposition
$T_{\mathbb{Q}}$ (see note 4)	Rational arithmetic (without multiplication), a.k.a. linear arithmetic.	$\Omega\left(2^n\right)$ (Fischer and Rabin) $O\left(2^{2^{kn}}\right)$ (Ferrante and Rackoff)	P (a.k.a. linear programming)	Ferrante and Rackoff’s Algorithm
$T^=_{\mathrm{A}}$ (see note 5)	Extensional Arrays	Undecidable	NP-complete (Stump et al.)	N/A

Notes on the table:

$T_{\mathrm{E}}$ is as defined in Bradley and Manna, that is it has a signature consisting of $=$ (equality) and all constant, function and predicate symbols, a.k.a. ‘equality with uninterpreted functions’. Reflexivity, symmetry, transitivity, function congruence and predicate congruence are axioms for $=$ , but all other functions and predicates are uninterpreted (except w.r.t. these congruence and predicate axioms). Note that this is not the theory of pure equality, for which the full theory is decidable and admits a weak form of quantifier elimination (pure equality doesn’t have the functions or predicates, see Bradley and Manna Section 10.4 for the definition of weak quantifier elimination).
Presburger arithmetic as described on Wikipedia does not admit quantifier elimination (counter-example: $\exists x. 2x = y$ ). However, adding an additional countable set of predicates capturing divisibility (one per divisor) together with an appropriate axiom leads to a version admitting quantifier elimination as per this table.
$T_{\mathbb{R}}$ is here taken to have a signature of $\{0, 1, +, -, \times, =, \geq\}$ (with $-$ unary) and axioms corresponding to those of a real closed field (theory of reals in SMT-LIB).
$T_{\mathbb{Q}}$ is here taken to have the signature $\{0, 1, +, -, = \geq\}$ (again with $-$ unary). Its axioms are those of an ordered torsion-free abelian group, together with an additional axiom schema asserting divisibility: $\forall x. \exists y. x = ny$ for every positive integer $n$ .
Using the notation of Bradley and Manna, the theory of extensional arrays is designed to capture array data structures. It has the signature $\{\cdot[\cdot], \cdot\langle\cdot\vartriangleleft\cdot\rangle, =\}$ , with the first two symbols denoting a binary and ternary function (respectively) for accessing and modifying array elements; arrays are immutable and so the ternary operator returns the modified array. ‘Extensional’ here denotes that there is an an axiom capturing that arrays are equal iff all their elements are equal in all places. (Theory of ArraysEx theory in SMT-LIB).

Further Comments

A decision procedure for the union of quantifier-free fragments can be obtained by combining the decision procedures for the individual fragments, via the Nelsen-Oppen method, under the following conditions:

Their signatures only share equality.
Their theories must (individually) be stably infinite, i.e. every $T$ -satisifiable quantifier-free formula is satisfied by a $T$ -interpretation with a domain of infinite cardinality.

If deciding each individual theory is in NP, then deciding the combination theory is also in NP.

While investigating the quantifier elimination column of the table above, I came across the Ultimate Eliminator tool which looks like great fun.

Please let me know if you spot any errors or significant omissions that may be of interest to readers of this blog.

Month: April 2022

Deciding Theories

Further Comments