Quantifiers

In a statement like x^4+x^2>0, the Wolfram Language treats the variable x as having a definite, though unspecified, value. Sometimes, however, it is useful to be able to make statements about whole collections of possible values for x. You can do this using quantifiers.

The structure of quantifiers.

You can work with quantifiers in the Wolfram Language much as you work with equations, inequalities, or logical connectives. In most cases, the quantifiers will not immediately be changed by evaluation. But they can be simplified or reduced by functions like (RefLink[FullSimplify, paclet:ref/FullSimplify]) and (RefLink[Reduce, paclet:ref/Reduce]).

This asserts that an x exists that makes the inequality true. The output here is just a formatted version of the input:

Exists[x,x^4+x^2>0]

(RefLink[FullSimplify, paclet:ref/FullSimplify]) establishes that the assertion is true:

FullSimplify[%]

This gives (RefLink[False, paclet:ref/False]), since the inequality fails when x is zero:

FullSimplify[ForAll[x,x^4+x^2>0]]

The Wolfram Language supports a version of the standard notation for quantifiers used in predicate logic and pure mathematics. You can input ∀ as \[(RefLink[ForAll, paclet:ref/ForAll])] or fa, and you can input ∃ as \[(RefLink[Exists, paclet:ref/Exists])] or ex. To make the notation precise, however, the Wolfram Language makes the quantified variable a subscript. The conditions on the variable can also be given in the subscript, separated by a comma.

Notation for quantifiers.

Given a statement that involves quantifiers, there are certain important cases where it is possible to resolve it into an equivalent statement in which the quantifiers have been eliminated. Somewhat like solving an equation, such quantifier elimination turns an implicit statement about what is true for all x or for some x into an explicit statement about the conditions under which this holds.

Quantifier elimination.

This shows that an x exists that makes the equation true:

Resolve[Exists[x,x^2==x^3]]

This shows that the equations can only be satisfied if c obeys a certain condition:

Resolve[Exists[x,x^2==c&&x^3==c+1]]

(RefLink[Resolve, paclet:ref/Resolve]) can always eliminate quantifiers from any collection of polynomial equations and inequations over complex numbers, and from any collection of polynomial equations and inequalities over real numbers. It can also eliminate quantifiers from Boolean expressions.

This finds the conditions for a quadratic form over the reals to be positive:

Resolve[ForAll[x,a x^2+b x+c>0],Reals]

This shows that there is a way of assigning truth values to p and q that makes the expression true:

Resolve[Exists[{p,q},p||q&&!q],Booleans]

You can also use quantifiers with (RefLink[Reduce, paclet:ref/Reduce]). If you give (RefLink[Reduce, paclet:ref/Reduce]) a collection of equations or inequalities, then it will try to produce a detailed representation of the complete solution set. But sometimes you may want to address a more global question, such as whether the solution set covers all values of x, or whether it covers none of these values. Quantifiers provide a convenient way to specify such questions.

This gives the complete structure of the solution set:

Reduce[x^2+x+c==0,{c,x},Reals]

This instead just gives the condition for a solution to exist:

Reduce[Exists[x,x^2+x+c==0],{c},Reals]

It is possible to formulate a great many mathematical questions in terms of quantifiers.

This finds the conditions for a circle to be contained within an arbitrary conic section:

Reduce[ForAll[{x,y},x^2+y^2<1,a x^2+b y^2<c],{a,b,c},Reals]

This finds the conditions for a line to intersect a circle:

Reduce[Exists[{x,y},x^2+y^2<1,r x+s y==1],{r,s},Reals]

This defines q to be a general monic quartic:

q[x_]:=x^4+b x^3+c x^2+d x+e

This finds the condition for all pairs of roots to the quartic to be equal:

Reduce[ForAll[{x,y},q[x]==0&&q[y]==0,x==y],{b,c,d,e}]

Although quantifier elimination over the integers is in general a computationally impossible problem, the Wolfram Language can do it in specific cases.

This shows that (Sqrt[2]) cannot be a rational number:

Resolve[Exists[{x,y},x^2==2 y^2&&y>0],Integers]

(Sqrt[9/4]) is, though:

Resolve[Exists[{x,y},4 x^2==9 y^2&&y>0],Integers]