WOLFRAM

Wolfram Language & System Documentation Center

ForAll[x,expr]

represents the statement that expr is True for all values of x.

ForAll[x,cond,expr]

states that expr is True for all x satisfying the condition cond.

ForAll[{x1,x2,…},expr]

states that expr is True for all values of all the xi.

Details
Details and Options Details and Options
Examples  
Basic Examples  
Scope  
Applications  
Properties & Relations  
See Also
Tech Notes
Related Guides
Related Links
History
Cite this Page

ForAll

ForAll[x,expr]

represents the statement that expr is True for all values of x.

ForAll[x,cond,expr]

states that expr is True for all x satisfying the condition cond.

ForAll[{x1,x2,…},expr]

states that expr is True for all values of all the xi.

Details

  • ForAll[x,expr] can be entered as ∀xexpr. The character ∀ can be entered as fa or \[ForAll]. The variable x is given as a subscript.
  • ForAll[x,cond,expr] can be entered as ∀x,condexpr.
  • In StandardForm, ForAll[x,expr] is output as ∀xexpr.
  • ForAll[x,cond,expr] is output as ∀x,condexpr.
  • ForAll can be used in such functions as Reduce, Resolve, and FullSimplify.
  • The condition cond is often used to specify the domain of a variable, as in x∈Integers.
  • ForAll[x,cond,expr] is equivalent to ForAll[x,Implies[cond,expr]].
  • ForAll[{x1,x2,…},…] is equivalent to .
  • The value of in ForAll[x,expr] is taken to be localized, as in Block.

Examples

open all close all

Basic Examples  (1)

This states that for all , is positive:

Wolfram Language code: ForAll[x, a x ^ 2 + b x + c > 0]

Use Resolve to get a condition on real parameters for which the statement is true:

Wolfram Language code: Resolve[%, Reals]

Reduce gives the condition in a solved form:

Wolfram Language code: Reduce[%%, {a, b, c}, Reals]

Scope  (6)

This states that for all the inequation is true:

Wolfram Language code: ForAll[x, x ^ 2 - x + 1 ≠ 0]

Use Resolve to prove that the statement is false:

Wolfram Language code: Resolve[%]

This states that for all real the inequation is true:

Wolfram Language code: ForAll[x, Element[x, Reals], x ^ 2 - x + 1 ≠ 0]

Use Resolve to prove that the statement is true:

Wolfram Language code: Resolve[%]

This states that for all pairs the inequality is true:

Wolfram Language code: ForAll[{x, y}, x ^ 2 + y ^ 2 ≥ 0]

With domain not specified, Resolve considers algebraic variables in inequalities to be real:

Wolfram Language code: Resolve[%]

With domain Complexes, complex values that make the inequality False are allowed:

Wolfram Language code: Resolve[%%, Complexes]

This states the tautology implies :

Wolfram Language code: ForAll[{p, q}, Implies[p && Implies[p, q], q]]

Prove it:

Wolfram Language code: Resolve[%]

If the expression does not explicitly contain a variable, ForAll simplifies automatically:

Wolfram Language code: ForAll[x, y == 0]
Wolfram Language code: ForAll[{x, y, z}, y == z]

TraditionalForm formatting:

Wolfram Language code: ForAll[x, p[x]]//TraditionalForm

Applications  (5)

This states the inequality between the arithmetic mean and the geometric mean:

Wolfram Language code: ForAll[{a, b}, a > 0 && b > 0, (a + b) / 2 ≥ Sqrt[a b]]

Use Resolve to prove the inequality:

Wolfram Language code: Resolve[%]

This states a special case of Hölder's inequality:

Wolfram Language code: ForAll[{a, b, c, d}, a > 0 && b > 0 && c > 0 && d > 0, a c + b d ≤ Sqrt[a ^ 2 + b ^ 2]Sqrt[c ^ 2 + d ^ 2]]

Use Resolve to prove the inequality:

Wolfram Language code: Resolve[%]

This states a special case of Minkowski's inequality:

Wolfram Language code: ForAll[{a, b, c, d}, Sqrt[(a + c) ^ 2 + (b + d) ^ 2] ≤ Sqrt[a ^ 2 + b ^ 2] + Sqrt[c ^ 2 + d ^ 2]]

Use Resolve to prove the inequality:

Wolfram Language code: Resolve[%]

Prove geometric inequalities for , , and sides of a triangle:

Wolfram Language code: triangle = a > 0 && b > 0 && c > 0 && a + b > c && a + c > b && b + c > a; acute = a ^ 2 + b ^ 2 > c ^ 2 && a ^ 2 + c ^ 2 > b ^ 2 && b ^ 2 + c ^ 2 > a ^ 2; s = 1 / 2(a + b + c); F = Sqrt[s(s - a)(s - b)(s - c)];

This states that an inequality is satisfied for all triangles:

Wolfram Language code: ForAll[{a, b, c}, triangle, a b c(a ^ 2 / b ^ 2 + b ^ 2 / c ^ 2 + c ^ 2 / a ^ 2) ≥ a ^ 3 + b ^ 3 + c ^ 3 + a b(b - a) + a c(a - c) + b c(c - b)]

Use Resolve to prove the inequality:

Wolfram Language code: Resolve[%]

This states that an inequality is satisfied for all acute triangles:

Wolfram Language code: ForAll[{a, b, c}, triangle && acute, 27(b ^ 2 + c ^ 2 - a ^ 2) ^ 2(a ^ 2 + c ^ 2 - b ^ 2) ^ 2(a ^ 2 + b ^ 2 - c ^ 2) ^ 2 ≤ (4F) ^ 6]

Use Resolve to prove the inequality:

Wolfram Language code: Resolve[%]

Test whether one region is included in another:

Wolfram Language code: R1 = (2x) ^ 2 + y ^ 2 + 2 x y ≤ 1; R2 = x ^ 2 + y ^ 2 ≤ 2;

This states that all points satisfying R1 also satisfy R2:

Wolfram Language code: ForAll[{x, y}, R1 R2]

The statement is true, hence the region defined by R1 is included in the region defined by R2:

Wolfram Language code: Resolve[%]

Plot the relationship:

Wolfram Language code: {r1, r2} = {RegionPlot[R1, {x, -2, 2}, {y, -2, 2}, PlotPoints -> 35, PlotStyle -> Pink], RegionPlot[R2, {x, -2, 2}, {y, -2, 2}]};
Wolfram Language code: Show[{r2, r1}]

Properties & Relations  (3)

Negation of ForAll gives Exists:

Wolfram Language code: !ForAll[x, x == a]
Wolfram Language code: !ForAll[x, Element[x, Reals], x == a]

Quantifiers can be eliminated using Resolve or Reduce:

Wolfram Language code: form = ForAll[{x, y}, Implies[a ≠ 0 && a x ^ 2 + b x + c == 0 && a y ^ 2 + b y + c == 0, x == y]]

This eliminates the quantifier:

Wolfram Language code: Resolve[form, Reals]

This eliminates the quantifier and solves the resulting equations and inequalities:

Wolfram Language code: Reduce[form, {a, b, c}, Reals]

This states that an equation is true for all complex values of :

Wolfram Language code: ForAll[x, (a - 2b + 1)x ^ 2 + (a - b ^ 2 - c)x == a ^ 2 - b + 3c - 1]

Use Reduce to find the values of parameters for which the statement is true:

Wolfram Language code: Reduce[%]

This solves the same problem using SolveAlways:

Wolfram Language code: SolveAlways[(a - 2b + 1)x ^ 2 + (a - b ^ 2 - c)x == a ^ 2 - b + 3c - 1, x]
Wolfram Research (2003), ForAll, Wolfram Language function, https://reference.wolfram.com/language/ref/ForAll.html.

Text

Wolfram Research (2003), ForAll, Wolfram Language function, https://reference.wolfram.com/language/ref/ForAll.html.

CMS

Wolfram Language. 2003. "ForAll." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/ForAll.html.

APA

Wolfram Language. (2003). ForAll. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/ForAll.html

BibTeX

@misc{reference.wolfram_2026_forall, author="Wolfram Research", title="{ForAll}", year="2003", howpublished="\url{https://reference.wolfram.com/language/ref/ForAll.html}", note=[Accessed: 13-June-2026]}

BibLaTeX

@online{reference.wolfram_2026_forall, organization={Wolfram Research}, title={ForAll}, year={2003}, url={https://reference.wolfram.com/language/ref/ForAll.html}, note=[Accessed: 13-June-2026]}