quantifier elimination
   HOME

TheInfoList



OR:

Quantifier elimination is a concept of simplification used in
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
,
model theory In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
, and
theoretical computer science Theoretical computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory. It is difficult to circumsc ...
. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such that \ldots?", and the statement without quantifiers can be viewed as the answer to that question. One way of classifying
formulas In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...
is by the amount of quantification. Formulas with less depth of quantifier alternation are thought of as being simpler, with the quantifier-free formulas as the simplest. A
theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be s ...
has quantifier elimination if for every formula \alpha, there exists another formula \alpha_ without quantifiers that is
equivalent Equivalence or Equivalent may refer to: Arts and entertainment *Album-equivalent unit, a measurement unit in the music industry * Equivalence class (music) *'' Equivalent VIII'', or ''The Bricks'', a minimalist sculpture by Carl Andre *''Equiva ...
to it ( modulo this theory).


Examples

An example from high school mathematics says that a single-variable
quadratic polynomial In mathematics, a quadratic polynomial is a polynomial of degree two in one or more variables. A quadratic function is the polynomial function defined by a quadratic polynomial. Before 20th century, the distinction was unclear between a polynomia ...
has a real root if and only if its
discriminant In mathematics, the discriminant of a polynomial is a quantity that depends on the coefficients and allows deducing some properties of the roots without computing them. More precisely, it is a polynomial function of the coefficients of the origi ...
is non-negative: :: \exists x\in\mathbb. (a\neq 0 \wedge ax^2+bx+c=0)\ \ \Longleftrightarrow\ \ a\neq 0 \wedge b^2-4ac\geq 0 Here the sentence on the left-hand side involves a quantifier \exists x\in\mathbb, while the equivalent sentence on the right does not. Examples of theories that have been shown decidable using quantifier elimination are
Presburger 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, omitti ...
,
algebraically closed field In mathematics, a field is algebraically closed if every non-constant polynomial in (the univariate polynomial ring with coefficients in ) has a root in . Examples As an example, the field of real numbers is not algebraically closed, because ...
s,
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. Def ...
s, atomless
Boolean algebras In abstract algebra, a Boolean algebra or Boolean lattice is a complemented distributive lattice. This type of algebraic structure captures essential properties of both set operations and logic operations. A Boolean algebra can be seen as a gen ...
,
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 exa ...
s,
dense linear order In mathematics, a partial order or total order < on a X is said to be dense if, for all x
s,
abelian group In mathematics, an abelian group, also called a commutative group, is a group in which the result of applying the group operation to two group elements does not depend on the order in which they are written. That is, the group operation is commut ...
s,
random graph In mathematics, random graph is the general term to refer to probability distributions over graphs. Random graphs may be described simply by a probability distribution, or by a random process which generates them. The theory of random graphs li ...
s, as well as many of their combinations such as Boolean algebra with Presburger arithmetic, and term algebras with queues. Quantifier eliminator for the theory of the real numbers as an ordered additive group is ''
Fourier–Motzkin elimination Fourier–Motzkin elimination, also known as the FME method, is a mathematical algorithm for eliminating variables from a system of linear inequalities. It can output real solutions. The algorithm is named after Joseph Fourier who proposed the me ...
''; for the theory of the field of real numbers it is the ''
Tarski–Seidenberg theorem In mathematics, the Tarski–Seidenberg theorem states that a set in (''n'' + 1)-dimensional space defined by polynomial equations and inequalities can be projected down onto ''n''-dimensional space, and the resulting set is still defina ...
''. Quantifier elimination can also be used to show that "combining" decidable theories leads to new decidable theories (see Feferman-Vaught theorem).


Algorithms and decidability

If a theory has quantifier elimination, then a specific question can be addressed: Is there a method of determining \alpha_ for each \alpha? If there is such a method we call it a quantifier elimination
algorithm In mathematics and computer science, an algorithm () is a finite sequence of rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algorithms are used as specificat ...
. If there is such an algorithm, then decidability for the theory reduces to deciding the truth of the quantifier-free
sentences ''The Four Books of Sentences'' (''Libri Quattuor Sententiarum'') is a book of theology written by Peter Lombard in the 12th century. It is a systematic compilation of theology, written around 1150; it derives its name from the ''sententiae'' o ...
. 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 first-order theory with quantifier elimination is
model complete In model theory, a first-order theory is called model complete if every embedding of its models is an elementary embedding. Equivalently, every first-order formula is equivalent to a universal formula. This notion was introduced by Abraham Robins ...
. Conversely, a model-complete theory, whose theory of universal consequences has the
amalgamation property In the mathematical field of model theory, the amalgamation property is a property of collections of structures that guarantees, under certain conditions, that two structures in the collection can be regarded as substructures of a larger one. Thi ...
, has quantifier elimination. The models of the theory of the universal consequences of a theory T are precisely the substructures of the models of T. The theory of linear orders does not have quantifier elimination. However the theory of its universal consequences has the amalgamation property.


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: :\exists x. \bigwedge_^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 literals, then if F is a quantifier-free formula, we can write it in
disjunctive normal form In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or (in philosophical logic) a ''cluster c ...
:\bigvee_^m \bigwedge_^n L_, and use the fact that :\exists x. \bigvee_^m \bigwedge_^n L_ is equivalent to :\bigvee_^m \exists x. \bigwedge_^n L_. Finally, to eliminate a 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.


Relationship with decidability

In early model theory, quantifier elimination was used to demonstrate that various theories possess 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 can be used to show that
Presburger 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, omitti ...
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 is decidable, and the
language Language is a structured system of communication. The structure of a language is its grammar and the free components are its vocabulary. Languages are the primary means by which humans communicate, and may be conveyed through a variety of met ...
of its valid formulas is
countable In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
, it is possible to extend the theory with countably many relations to have quantifier elimination (for example, one can introduce, for each formula of the theory, a relation symbol that relates the
free variable In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not ...
s of the formula). Example: Nullstellensatz for
algebraically closed field In mathematics, a field is algebraically closed if every non-constant polynomial in (the univariate polynomial ring with coefficients in ) has a root in . Examples As an example, the field of real numbers is not algebraically closed, because ...
s and for
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 . Differ ...
s.


See also

*
Cylindrical algebraic decomposition In mathematics, cylindrical algebraic decomposition (CAD) is a notion, and an algorithm to compute it, that are fundamental for computer algebra and real algebraic geometry. Given a set ''S'' of polynomials in R''n'', a cylindrical algebraic decom ...
*
Elimination theory Elimination may refer to: Science and medicine *Elimination reaction, an organic reaction in which two functional groups split to form an organic product *Bodily waste elimination, discharging feces, urine, or foreign substances from the body ...
*
Conjunction elimination In propositional logic, conjunction elimination (also called ''and'' elimination, ∧ elimination, or simplification)Hurley is a valid immediate inference, argument form and rule of inference which makes the inference that, if the conjunction ' ...


Notes


References

* * * * * * * * *, see for an English translation * * * {{Refend Model theory