# 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*.

ForAll[x,expr] | expr holds for all values of x |

ForAll[{x_{1},x_{2},…},expr] | exprholds for all values of all thex_{i} |

ForAll[{x_{1},x_{2},…},cond,expr] | exprholds for allx_{i}satisfyingcond |

Exists[x,expr] | there exists a value of x for which expr holds |

Exists[{x_{1},x_{2},…},expr] | there exist values of the x_{i} for which expr holds |

Exists[{x_{1},…},cond,expr] | there exist values of the x_{i} satisfying cond for which expr holds |

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 FullSimplify and Reduce.

The Wolfram Language supports a version of the standard notation for quantifiers used in predicate logic and pure mathematics. You can input as \[ForAll] or EscfaEsc, and you can input as \[Exists] or EscexEsc. 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.

∀_{x}expr | ForAll[x,expr] |

∀_{{x1,x2,…}}expr | ForAll[{x_{1},x_{2},…},expr] |

∀_{x,cond}expr | ForAll[x,cond,expr] |

∃_{x}expr | Exists[x,expr] |

∃_{{x1,x2,…}}expr | Exists[{x_{1},x_{2},…},expr] |

∃_{x,cond}expr | Exists[x,cond,expr] |

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.

Resolve[expr] | attempt to eliminate quantifiers from expr |

Resolve[expr,dom] | attempt to eliminate quantifiers with all variables assumed to be in domain dom |

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.

You can also use quantifiers with Reduce. If you give 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.

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

In[12]:= |

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