Skip to content
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.

exists(p: person(p) and age[p] > 99)
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))

Next: Universal Quantification

Was this doc helpful?