Quantifier elimination

Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement ' ∃ x {displaystyle exists x} such that … {displaystyle ldots } ' can be viewed as a question 'When is there an x {displaystyle x} such that … {displaystyle ldots } ?', and the statement without quantifiers can be viewed as the answer to that question. Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement ' ∃ x {displaystyle exists x} such that … {displaystyle ldots } ' can be viewed as a question 'When is there an x {displaystyle x} such that … {displaystyle ldots } ?', and the statement without quantifiers can be viewed as the answer to that question. One way of classifying formulas is by the amount of quantification. Formulas 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 α {displaystyle alpha } , there exists another formula α Q F {displaystyle alpha _{QF}} without quantifiers that is equivalent to it (modulo this theory). An example from high school mathematics says that a single-variable quadratic polynomial has a real root if and only if its discriminant is non-negative: Examples of theories that have been shown decidable using quantifier elimination are Presburger arithmetic, algebraically closed fields, real closed fields, atomless Boolean algebras, term algebras, dense linear orders, abelian groups, random graphs 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; for the theory of the field of real numbers it is the Tarski–Seidenberg theorem. Quantifier elimination can also be used to show that 'combining' decidable theories leads to new decidable theories. If a theory has quantifier elimination, then a specific question can be addressed: Is there a method of determining α Q F {displaystyle alpha _{QF}} for each α {displaystyle alpha } ? 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.