Quantifier elimination
Encyclopedia
Quantifier elimination is a concept of simplification used in mathematical logic
, model theory
, and theoretical computer science
. One way of classifying formulas
is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulae as the simplest.
A theory has quantifier elimination if for every formula
, there exists another formula 
without quantifiers which is equivalent
to it (modulo
the theory).
, real closed field
s, atomless Boolean algebras, term algebra
s, dense linear orders, random graph
s,
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 the Feferman-Vaught theorem and Term Powers.
for each 
? If there is such a method we call it a quantifier elimination algorithm
. If there is such an algorithm, then decidability for the theory reduces to deciding the truth of the quantifier-free sentences
. Quantifier-free sentences have no variables, so their validity in a given theory can often be computed, which enables the use of quantifier elimination algorithms to decide validity of sentences.
Every theory with quantifier elimination is model complete.
A first-order theory T has quantifier elimination if and only if for any two models B and C of T and for any common substructure A of B and C, B and C are elementarily equivalent in the language of T augmented with constants from A. In fact, it is sufficient here to show that any sentence with only existential quantifiers have the same truth value in B and C.
, 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 formulae, 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
Theories could be decidable yet not admit quantifier elimination. Strictly speaking, the theory of the additive natural numbers did not admit quantifier elimination, but it was an expansion of the additive natural numbers that was shown to be decidable. Whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations
to ensure that it admits quantifier elimination (for example, one can introduce a relation symbol for each formula).
Example: Nullstellensatz in ACF
and DCF
.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
, and theoretical computer science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
. One way of classifying formulas
Well-formed formula
In mathematical logic, a well-formed formula, shortly wff, often simply formula, is a word which is part of a formal language...
is by the amount of quantification. Formulae with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulae as the simplest.
A theory has quantifier elimination if for every formula
, there exists another formula without quantifiers which is equivalentLogical equivalence
In logic, statements p and q are logically equivalent if they have the same logical content.Syntactically, p and q are equivalent if each can be proved from the other...
to it (modulo
Modulo
In the mathematical community, the word modulo is often used informally. Generally, to say "A is the same as B modulo C" means, more-or-less, "A and B are the same except for differences accounted for or explained by C"....
the theory).
Examples
Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmeticPresburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitting the multiplication operation entirely...
, real closed field
Real closed field
In mathematics, a real closed field is a field F that has the same first-order properties as the field of real numbers. Some examples are the field of real numbers, the field of real algebraic numbers, and the field of hyperreal numbers.-Definitions:...
s, atomless Boolean algebras, term algebra
Term algebra
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
s, dense linear orders, random graph
Random graph
In mathematics, a random graph is a graph that is generated by some random process. The theory of random graphs lies at the intersection between graph theory and probability theory, and studies the properties of typical random graphs.-Random graph models:...
s,
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
Decidability (logic)
In logic, the term decidable refers to the decision problem, the question of the existence of an effective method for determining membership in a set of formulas. Logical systems such as propositional logic are decidable if membership in their set of logically valid formulas can be effectively...
theories leads to new decidable theories. Such constructions include the Feferman-Vaught theorem and Term Powers.
Algorithms and decidability
If a theory has quantifier elimination, then a specific question can be addressed: Is there a method of determining for each ? If there is such a method we call it a quantifier elimination algorithmAlgorithm
In mathematics and computer science, an algorithm is an effective method expressed as a finite list of well-defined instructions for calculating a function. Algorithms are used for calculation, data processing, and automated reasoning...
. If there is such an algorithm, then decidability for the theory reduces to deciding the truth of the quantifier-free sentences
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
. Quantifier-free sentences have no variables, so their validity in a given theory can often be computed, which enables the use of quantifier elimination algorithms to decide validity of sentences.
Related concepts
Various model theoretic ideas are related to quantifier elimination, and there are various equivalent conditions.Every theory with quantifier elimination is model complete.
A first-order theory T has quantifier elimination if and only if for any two models B and C of T and for any common substructure A of B and C, B and C are elementarily equivalent in the language of T augmented with constants from A. In fact, it is sufficient here to show that any sentence with only existential quantifiers have the same truth value in B and C.
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 literalsLiteral (mathematical logic)
In mathematical logic, a literal is an atomic formula or its negation.The definition mostly appears in proof theory , e.g...
, 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 formulae, then if is a quantifier-free formula, we can write it in disjunctive normal formDisjunctive normal form
In boolean logic, a disjunctive normal form is a standardization of a logical formula which is a disjunction of conjunctive clauses. As a normal form, it is useful in automated theorem proving. A logical formula is considered to be in DNF if and only if it is a disjunction of one or more...
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
History
In early model theory, quantifier elimination was used to demonstrate that various theories possess certain model-theoretic properties like decidability and completeness. A common technique was to show first that a theory admits elimination of quantifiers and thereafter prove decidability or completeness by considering only the quantifier-free formulas. This technique is used to show that Presburger arithmetic, i.e. the theory of the additive natural numbers, is decidable.Theories could be decidable yet not admit quantifier elimination. Strictly speaking, the theory of the additive natural numbers did not admit quantifier elimination, but it was an expansion of the additive natural numbers that was shown to be decidable. Whenever a theory in a countable language is decidable, it is possible to extend its language with countably many relations
Relation (mathematics)
In set theory and logic, a relation is a property that assigns truth values to k-tuples of individuals. Typically, the property describes a possible connection between the components of a k-tuple...
to ensure that it admits quantifier elimination (for example, one can introduce a relation symbol for each formula).
Example: Nullstellensatz in ACF
Algebraically closed field
In mathematics, a field F is said to be algebraically closed if every polynomial with one variable of degree at least 1, with coefficients in F, has a root in F.-Examples:...
and DCF
Differentially closed field
In mathematics, a differential field K is differentially closed if every finite system of differential equations with a solution in some differential field extending K already has a solution in K. This concept was introduced by...
.