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.

Next: Universal Quantification