Quantifier elimination

From Wikipedia, the free encyclopedia

Quantifier elimination is a technique in 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.

[edit] Basic Ideas

To constructively show 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: $\exists x. \bigwedge_{i=1}^n L_i$ where each $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 $F$ is a quantifier-free formula, we can write it in disjunctive normal form $\bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij}$ , and use the fact that $\exists x. \bigvee_{j=1}^m \bigwedge_{i=1}^n L_{ij}$ is equivalent to $\bigvee_{j=1}^m \exists x. \bigwedge_{i=1}^n L_{ij}$ . Finally, to eliminate universal quantifier $\forall x. F$ where $F$ is quantifier-free, we transform $\lnot F$ into disjunctive normal form, and use the fact that $\forall x. F$ is equivalent to $\lnot \exists x. \lnot F.$

[edit] 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.