Exists
Details
- Exists[x,expr] can be entered as
. The character 
can be entered as 
ex
or \[Exists]. The variable 
is given as a subscript. - Exists[x,cond,expr] can be entered as
. - In StandardForm, Exists[x,expr] is output as
. - Exists[x,cond,expr] is output as
. - Exists 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.
- Exists[x,cond,expr] is equivalent to Exists[x,cond&&expr].
- Exists[{x1,x2,…},…] is equivalent to
. - The value of
in Exists[x,expr] is taken to be localized, as in Block.
Examples
open all close allBasic Examples (1)
This states that there exists a positive solution to the equation 
:
Exists[x, a x ^ 2 + b x + c == 0 && x > 0]Use Resolve to get a condition on real parameters for which the statement is true:
Resolve[%, Reals]Reduce gives the condition in a solved form:
Reduce[%%, {a, b, c}, Reals]Scope (6)
This states that there exists 
for which the equation is true:
Exists[x, x ^ 2 - x + 1 == 0]Use Resolve to prove that the statement is true:
Resolve[%]This states that there exists a real 
for which the equation is true:
Exists[x, Element[x, Reals], x ^ 2 - x + 1 == 0]Use Resolve to prove that the statement is false:
Resolve[%]This states that there exists a pair 
for which the inequality is true:
Exists[{x, y}, x ^ 2 + y ^ 2 < 0]With domain not specified, Resolve considers algebraic variables in inequalities to be real:
Resolve[%]With domain Complexes, complex values that make the inequality True are allowed:
Resolve[%%, Complexes]This states that the negation of a tautology is satisfiable:
Exists[{p, q}, !Implies[p && Implies[p, q], q]]Use Resolve to prove it False:
Resolve[%]If the expression does not explicitly contain the variable, Exists simplifies automatically:
Exists[x, y == 0]Exists[{x, y, z}, y == z]TraditionalForm formatting:
Exists[x, p[x]]//TraditionalFormApplications (4)
This states that a quadratic attains negative values:
Exists[x, a x ^ 2 + b x + c < 0]This gives explicit conditions on real parameters:
Resolve[%, Reals]Test whether one region is included in another:
R1 = (2x) ^ 2 + y ^ 2 + 2 x y ≤ 1;
R2 = x ^ 2 + y ^ 2 ≤ 2;This states that there are points satisfying R1 and not R2:
Exists[{x, y}, Element[x | y, Reals], R1 && !R2]The statement is false, hence the region defined by R1 is included in the region defined by R2:
Resolve[%]{r1, r2} = {RegionPlot[R1, {x, -2, 2}, {y, -2, 2}, PlotPoints -> 35, PlotStyle -> Pink], RegionPlot[R2, {x, -2, 2}, {y, -2, 2}]};Show[{r2, r1}]triangle = a > 0 && b > 0 && c > 0 && a + b > c && a + c > b && b + c > a;
s = 1 / 2(a + b + c);
F = Sqrt[s(s - a)(s - b)(s - c)];
conjecture = 27(b ^ 2 + c ^ 2 - a ^ 2) ^ 2(a ^ 2 + c ^ 2 - b ^ 2) ^ 2(a ^ 2 + b ^ 2 - c ^ 2) ^ 2 ≤ (4F) ^ 6;This states that there is a triangle for which the conjecture is not true:
Exists[{a, b, c}, Element[a | b | c, Reals], triangle && !conjecture]The statement is true, hence the conjecture is not true for arbitrary triangles:
Resolve[%]This states that there is an acute triangle for which the conjecture is not true:
acute = a ^ 2 + b ^ 2 > c ^ 2 && a ^ 2 + c ^ 2 > b ^ 2 && b ^ 2 + c ^ 2 > a ^ 2;Exists[{a, b, c}, Element[a | b | c, Reals], triangle && acute && !conjecture]The statement is false, hence the conjecture is true for all acute triangles:
Resolve[%]Prove that a statement is a tautology:
statement = (a && ((a && !(b || (a && c))) || b || (a && c))) || !a || !((a && !(b || (a && c))) || b || (a && c));This proves that there are no values of 
for which the statement is not true:
Resolve[Exists[{a, b, c}, !statement]]This can be proven with TautologyQ as well:
TautologyQ[statement]Properties & Relations (5)
Negation of Exists gives ForAll:
!Exists[x, x == a]!Exists[x, Element[x, Reals], x == a]Quantifiers can be eliminated using Resolve or Reduce:
form = Exists[{x, y}, x ≠ y && a x ^ 2 + b x + c == 0 && a y ^ 2 + b y + c == 0]This eliminates the quantifier:
Resolve[form, Reals]This eliminates the quantifier and solves the resulting equations and inequalities:
Reduce[form, {a, b, c}, Reals]This shows that a system of inequalities has solutions:
ineqs = x ^ 2 + y ^ 2 < 2 && (x - 1) ^ 2 + (y - 1) ^ 2 < 2Resolve[Exists[{x, y}, ineqs], Reals]Use FindInstance to find an explicit solution instance:
FindInstance[ineqs, {x, y}, Reals]This states that there exists a complex 
for which the equations are satisfied:
Exists[x, x ^ 2 + y ^ 2 + z ^ 2 == 1 && x y == z ^ 3]Use Resolve to find conditions on 
and 
for which the statement is true:
Resolve[%]This solves the same problem using Eliminate:
Eliminate[x ^ 2 + y ^ 2 + z ^ 2 == 1 && x y == z ^ 3, x]This finds the projection of the complex algebraic set 
along the 
axis:
Reduce[Exists[y, x y == 1], x]This finds the projection of the real unit disc along the 
axis:
Reduce[Exists[y, x ^ 2 + y ^ 2 ≤ 1], x, Reals]Related Links
NKS|OnlineText
Wolfram Research (2003), Exists, Wolfram Language function, https://reference.wolfram.com/language/ref/Exists.html.
CMS
Wolfram Language. 2003. "Exists." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/Exists.html.
APA
Wolfram Language. (2003). Exists. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/Exists.html