# Deciding Theories

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.

Notes on the table:

1. $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).
2. 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.
3. $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).
4. $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$.
5. 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).

2. 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.