REL
REFERENCE
Existential Quantification

# Existential Quantification

``````Expr := "exists" Expr
| "∃" Expr``````

The value of an existential quantification is `false` if the argument evaluates to the empty relation, and `true` otherwise. 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 `x` and `y` such that `x` belongs to `P`, `y` belongs to the first column of `Q`, and `x` is greater than `y`.” 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`.

Examples
`exists(p: person(p) and age[p] > 99)`
`exists(centenarian)`
`∃(centenarian)`
`c: course(c) and not ∃(s: enrolled(c, s))`
`c: course(c) and not ∃(enrolled[c])`
`def grandparent(a, b) = exists(t: parent(a, t) and parent(t, b))`