Quantifier elimination

Quantifier elimination is a simplification method in mathematical logic, model theory, and theoretical computer science. Roughly speaking, a quantified statement like "there exists an \(x\) such that ..." can be seen as asking "When is there an \(x\) such that ...?", and the equivalent statement without quantifiers gives the answer. Formulas are often classified by how much quantification they contain; those with fewer alternations between quantifiers are considered simpler, and quantifier-free formulas are the simplest kind. A theory is said to have quantifier elimination if, for any formula, there is a quantifier-free formula that is equivalent to it within that theory.

Examples

For example, a quadratic polynomial in one variable has a real root exactly when its discriminant is non-negative. This means two sentences—one using a quantifier and the other without—define the same set of triples of real numbers.

Theories shown to be decidable using quantifier elimination include Presburger arithmetic, Skolem arithmetic, algebraically closed fields, real closed fields, atomless Boolean algebras, term algebras, dense linear orders, abelian groups, Rado graphs, and combinations like Boolean algebra with Presburger arithmetic or term algebras with queues. For the real numbers as an ordered additive group, quantifier elimination is achieved by Fourier–Motzkin elimination; for the real numbers as a field, it is given by the Tarski–Seidenberg theorem. Quantifier elimination can also show that combining decidable theories yields new decidable theories, as in the Feferman–Vaught theorem.

Algorithms and decidability

If a theory has quantifier elimination, one can ask whether there is a method to produce the quantifier-free equivalent for each formula. Such a method is a quantifier elimination algorithm. If one exists, deciding the truth of quantifier-free sentences determines the decidability of the whole theory.

Related concepts

Several model-theoretic concepts relate to quantifier elimination, with various equivalent conditions. Any first-order theory with quantifier elimination is model complete.

Conversely, a model-complete theory whose theory of universal consequences has the amalgamation property also has quantifier elimination. The models of the theory of the universal consequences of a theory are exactly the substructures of the models of that theory. The theory of linear orders does not have quantifier elimination, but the theory of its universal consequences does have the amalgamation property.

Basic ideas

To show constructively that a theory has quantifier elimination, it is enough to eliminate an existential quantifier applied to a conjunction of literals—that is, to show that any formula of the form \(\exists x (L_1 \land \dots \land L_n)\), where each \(L_i\) is a literal, is equivalent to a quantifier-free formula. If this is possible, then for any quantifier-free formula \(F\), write it in disjunctive normal form and use the fact that \(\exists x (D_1 \lor \dots \lor D_k)\) is equivalent to \(\exists x D_1 \lor \dots \lor \exists x D_k\). To eliminate a universal quantifier \(\forall x F\) with \(F\) quantifier-free, transform \( eg F\) into disjunctive normal form and use the equivalence of \(\forall x F\) with \( eg \exists x eg F\).

In early model theory, quantifier elimination was used to show that theories are decidable or complete. The typical approach was to first prove that a theory admits quantifier elimination, then decide truth using only quantifier-free formulas. This method shows, for instance, that Presburger arithmetic is decidable.

Some theories are decidable but do not admit quantifier elimination. Strictly speaking, the theory of additive natural numbers did not, but an expansion of it was shown decidable. Whenever a theory \(T\) is decidable and its valid formulas form a countable language, it can be extended with countably many relation symbols to have quantifier elimination—for example, by introducing a relation symbol for each formula that relates its free variables.

An example of this concept in action is the Nullstellensatz for algebraically closed fields and for differentially closed fields.