Universal Quantification

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

ExamplesDescription
`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