Quantifier elimination

Quantifier elimination is a technique in mathematical logic, model theory, and theoretical computer science. We say that a given theory has quantifier elimination if for every sentence with quantification there exists an equivalent (modulo the theory) sentence without quantifiers.

In model theory, quantifier elimination has several alternative characterizations, and does not necessarily imply the existence of a quantifier elimination algorithm.

A quantifier elimination algorithm for a given theory transforms formulas with quantifiers into equivalent formulas without quantifiers. Using a quantifier elimination algorithm we can transform every sentence (formula with no free variables) into an equivalent formula with no variables, which can be usually decided by simple computation. Therefore, a quantifier elimination algorithm for a theory typically implies the decidability of the theory.

Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmetic, real closed fields, atomless Boolean algebras, term algebras, dense linear orders, random graphs, Feature trees, as well as many of their combinations such as Boolean Algebra with Presburger arithmetic, and Term Algebras with Queues. Quantifier elimination can also be used to show that "combining" decidable theories leads to new decidable theories. Such constructions include Feferman-Vaught theorem and Term Powers.

Basic ideas

To show constructively that a theory has quantifier elimination, it suffices to show that we can eliminate an existential quantifier applied to a conjunction of literals, that is, show that each formula of the form:

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists x. \bigwedge_{i=1}^n L_i

where each Failed to parse (Missing texvc executable; please see math/README to configure.): L_i

is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of formulas, then if Failed to parse (Missing texvc executable; please see math/README to configure.): F
is a quantifier-free formula, we can write it in disjunctive normal form 

Failed to parse (Missing texvc executable; please see math/README to configure.): \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij},

and use the fact that

Failed to parse (Missing texvc executable; please see math/README to configure.): \exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij}

is equivalent to

Failed to parse (Missing texvc executable; please see math/README to configure.): \bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij}.

Finally, to eliminate a universal quantifier

Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x. F

where Failed to parse (Missing texvc executable; please see math/README to configure.): F

is quantifier-free, we transform 

Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot F

into disjunctive normal form, and use the fact that Failed to parse (Missing texvc executable; please see math/README to configure.): \forall x. F

is equivalent to Failed to parse (Missing texvc executable; please see math/README to configure.): \lnot \exists x. \lnot F.

References

• Wilfrid Hodges. "Model Theory". Cambridge University Press. 1993.
• Viktor Kuncak and Martin Rinard. "Structural Subtyping of Non-Recursive Types is Decidable". In Eighteenth Annual IEEE Symposium on Logic in Computer Science, 2003.

This mathematics-related article is a stub. You can help Wikipedia by expanding it.

ru:Элиминация кванторов