- 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.
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 usually be 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 theoremand Term Powers.
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:
where each is a literal, is equivalent to a quantifier-free formula. Indeed, suppose we know how to eliminate quantifiers from conjunctions of formulas, then if is a quantifier-free formula, we can write it in
disjunctive normal form
and use the fact that
is equivalent to
Finally, to eliminate a universal quantifier
where is quantifier-free, we transform into disjunctive normal form, and use the fact that is equivalent to
* 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.
Wikimedia Foundation. 2010.