Universal Quantification

Expr := "forall" "(" Bindings ":" Expr ")"
      | "∀"      "(" Bindings ":" Expr ")"

The argument of universal quantification consists of one or more bindings, followed by a colon and an expression. The expression must be a formula, that is, it must evaluate to a relation of arity 0.

The universal quantification is true if the expresssion that follows the : is true for all values of the variables specified in the bindings.

In other words, the universal quantification is true if there is no combination of values for the variables specified in the bindings such that the expression that follows the : is false.

To put it more succinctly: forall(bindings : E) is equivalent to not exists(bindings : not E).

An important consequence of this is that if the domain of any of the variables is empty, the universal quantification evaluates to true.

Consider the following example:

// read query
 
def P = 1; 3; 5; 7
def Q = (6, 8); (7, 9)
def R = x : P(x) and Q(_, x)
def output:A = forall(x in P, y in Q[_] : x < y)
def output:B = forall(x in P, y where Q(y, _) : x < y)
def output:C = forall(x in R, y where Q(y, _) : x < y)
def output:D = not exists(x in R, y where Q(y, _) : not(x < y))
def output:E = R

For every x in P and every y in the second column of Q, x is smaller than y, so relation output:A is true. Relation output:B is false, because it is not true that, for every x in P and every y in the first column of Q, x is smaller than y. However, relation output:C is true, because the domain of x is empty, as shown by the fact that output:E is false. Relation output:D is true, because there does not exist any x in R, so the existential quantification evaluates to false. The definition of output:D is equivalent to the definition of output:C.

The bindings usually define the domains of the variables, but this is not required:

// read query
 
def P = 1; 3; 5; 7
def Q = (6, 8); (7, 9)
def output = forall(x, y: P(x) and Q[_] = y implies x < y)

The definition of output is equivalent to the definition of output:A in the previous example.

In general, you should prefer forall x, y,... where E1(x, y,...) : E2 to forall x, y,... : E1(x, y,...) implies E2. For many people the first form is much easier to read.

Next: Aggregation