# 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.

Examples | Description |
---|---|

`forall(p in person: age[p] > 99)` | Are all persons older than 99? |

`∀(p in person: centenarian(p))` | Are all persons centenarians? This expression features a Unicode “forall” quantifier. |

`exists(c in course: forall(s in student: enrolled(c, s))` | Does there exist a course where all students are enrolled? |

`∃(c in course: ∀(s in student: enrolled(c, s))` | Same, with Unicode quantifiers. |

`c: course(c) and ∀(y in year: ∀(s where class[s] = y: enrolled(c, s)))` | Courses that have, for every year, all students from that year enrolled. |

`c: course(c) and ∃(y in year: ∀(s where class[s] = y: enrolled(c, s)))` | Courses that have all students from some year enrolled. |

Next: Aggregation