Quantifier elimination

Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "${\displaystyle \exists x}$ such that ..." can be viewed as a question "When is there an ${\displaystyle x}$ such that ...?", 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 formulas as the simplest. A theory has quantifier elimination if for every formula ${\displaystyle \alpha }$, there exists another formula ${\displaystyle \alpha _{QF}}$ without quantifiers that is equivalent to it (modulo this theory).

An example from mathematics says that a single-variable quadratic polynomial has a real root if and only if its discriminant is non-negative:

$${\displaystyle \exists x\in \mathbb {R} .(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 ${\displaystyle \exists x\in \mathbb {R} }$, whereas the equivalent sentence on the right does not.

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, Rado graphs, as well as many of their combinations such as Boolean algebra with Presburger arithmetic, and term algebras with queues.

Quantifier elimination 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 (see Feferman–Vaught theorem).