Expr := "exists" Expr | "∃" Expr
The value of an existential quantification is
false if the argument evaluates to the empty relation, and
The argument can be an expression of any arity.
The argument of an existential quantification is often a relational abstraction. The effect is very similar to conventional existential quantification. Consider the following example:
// read query def P = 1; 3; 5 def Q = (2, 4); (6, 8) def output:RA = x, y : P(x), Q[y], x > y def output:EX = exists(x, y : P(x), Q[y], x > y)
You can read the body of the definition of
output:EX as “there exist
y such that
x belongs to
y belongs to the first column of
x is greater than
This evaluates to
true, as expected.
What really happens here is that the relational abstraction that is the argument of
exists evaluates to a nonempty relation.
You could get exactly the same result with
def output:EX = exists output:RA.
Next: Universal Quantification