Quantifier Elimination

Quantifier elimination is the removal of all quantifiers (the universal quantifier and existential quantifier ) from a quantified system. A first-order theory allows quantifier elimination if, for each quantified formula, there exists an equivalent quantifier-free formula. Examples of such theories include the real numbers with , , , and , and the complex numbers with , , and . For example, over the real numbers,

(1)

Here is a free variable, and the quantifier-free condition describes precisely the values of for which the original formula holds. When there are no free variables, elimination instead determines the truth value of a sentence (Basu 2017, p. 109).

For an example involving a strict inequality, over the real numbers,

(2)

Here is a free variable, and the equivalence follows from the strict monotonicity of . An example with a universal quantifier is

(3)

where , , and are real and and are free variables. This equivalence follows by completing the square.

The domain of the variables is essential. Over the complex numbers, the formula holds for every . For integer variables with addition and multiplication, there is no general algorithm for quantifier elimination. Such a procedure would decide whether an arbitrary polynomial in several variables with integer coefficients vanishes at a point with all coordinates in the integers, contrary to the negative solution of Hilbert's tenth problem (Matiyasevich 1993, 2004). Individual integer statements may still be easy to decide. For example, the assertion that has integer solutions and for every positive integer is false at , whereas the assertion with real and is true.

For a finite system of linear inequalities with constant real coefficients, Fourier-Motzkin elimination removes a variable by comparing every lower bound with every upper bound and retaining the inequalities independent of that variable (Dantzig and Eaves 1973). Repeated elimination therefore describes coordinate projections of the solution set using linear inequalities. For a matrix with bounded entries, the possible row, column, and diagonal sums are another example of such a projection. With independent closed interval bounds, these sums form a zonotope, since they are an image of a hypercube under an affine transformation (Trott 2006).

A geometric intersection test also gives a quantified formula. Consider an open axis-aligned square with side length 2 and center , and an open disk of radius 1 with center , where (Trott 2006). The horizontal coordinates of their centers agree, so their interiors intersect iff

(4)

Eliminating shows that an intersection occurs at some real time iff . At , the two boundaries touch at , while the interiors remain disjoint.

A definition involving alternating quantifiers can also be used to compute a limit. For example, consider the rational function

(5)

For a real number , the assertion can be written as

(6)

where all quantified variables range over the real numbers. The denominator is positive for , so clearing it preserves the inequalities. The resulting formula contains only polynomials and inequalities. Eliminating , , and gives

(7)

The free variable is the unknown limit rather than a variable to eliminate (Trott 2006).

Quantifier elimination is implemented in the Wolfram Language as Resolve[expr].

General real quantifier elimination has doubly exponential worst-case complexity, with examples requiring doubly exponential output size (Davenport and Heintz 1988, Caviness and Johnson 1998). The number of quantifier alternations matters. For a fixed number of blocks, algorithms with singly exponential dependence on the number of variables are available (Basu 2017).