Nested Quantifiers and Specifications

From one quantifier to two

Last week every statement had a single quantifier: “every student has taken Java”, “some server is overloaded”. That was enough to talk about properties of individual things. But many of the most interesting statements in computing are about relationships between things, and a relationship has two sides.

Think about a social network. “Everyone follows someone” talks about two people at once: the follower and the one being followed. So does “every user has a password”, “every request is answered by some server”, and “for every number there is a bigger one”. To write any of these we need a predicate with two variables, and a quantifier for each of them. When one quantifier sits inside the scope of another, we call them nested quantifiers.

Nothing new is needed to understand them. A nested statement is simply a quantified statement whose body is itself a quantified statement. You can always read it in two steps. In $\forall x\, \exists y\; P(x, y)$, first fix one particular $x$; the part $\exists y\; P(x, y)$ is then an ordinary week 4 statement about that one $x$. The outer $\forall x$ asks whether this inner statement holds for every choice of $x$.

Nested quantifiers are nested loops

If you have written a loop inside a loop, you already know how to evaluate a nested statement over a finite domain. Here is “everyone follows someone”, with $F(x, y)$ meaning “$x$ follows $y$”:

def everyone_follows_someone(people, F):
    for x in people:                 # ∀x : check every person ...
        found = False
        for y in people:             #   ∃y : ... has at least one y
            if F(x, y):
                found = True
                break                #   witness found for this x, move on
        if not found:
            return False             # this x is a counterexample
    return True

The outer loop is the $\forall$, the inner loop is the $\exists$. In Python the same thing fits on one line, and reading the line from the outside in gives exactly the logic:

all(any(F(x, y) for y in people) for x in people)     # ∀x ∃y F(x, y)

Notice that the inner loop runs once for each $x$. Over a domain of $n$ people, a nested statement may look at up to $n \times n$ pairs. That is why checking such statements on large data is expensive, a theme we return to when we study algorithms.

Two quantifiers of the same kind

When both quantifiers are the same, their order does not matter. “For every $x$ and every $y$” covers every pair no matter which variable you pick first, just as a double loop visits every cell of a table whether you go row by row or column by column. The same is true for two existentials: “there is an $x$ and there is a $y$” only asks for one suitable pair.

For example, over the real numbers, $\forall x\, \forall y\; (x + y = y + x)$ states that addition is commutative, and it is true. The statement $\exists x\, \exists y\; (x + y = 10 \land x - y = 4)$ asks whether the system of two equations has a solution, and it does: $x = 7$, $y = 3$.

When the order matters

The real subtlety begins when the quantifiers are mixed. Compare these two statements, where the domain is all integers:

The first one says: whatever integer $x$ you give me, I can find a $y$ that brings the sum to 10. That is true, because I simply choose $y = 10 - x$. The important detail is that my choice of $y$ depends on your $x$: for $x = 3$ I answer 7, for $x = 12$ I answer $-2$.

The second one says something much stronger: there is a single integer $y$ that works for every $x$ at the same time. There is no such number. If $y$ makes $1 + y = 10$, then $y = 9$, and $2 + 9 \ne 10$. The second statement is false.

Seeing it in a network

The grid below shows a small network of five people. A 1 in row $x$ and column $y$ means “$x$ follows $y$”. Choose a statement, read the explanation, and click cells to change who follows whom. The most useful exercise is to compare the first two buttons.

The grid turns the abstract difference into a picture. $\forall x\, \exists y\; F(x, y)$ says that every row contains at least one 1: each person follows somebody, and each row may find its 1 in a different place. $\exists y\, \forall x\; F(x, y)$ says that some column is completely filled: one person, the same for everyone, is followed by all the others. In the starting network, every row has a 1 but no column is full, so the first statement is true and the second is false. If you make everyone follow Ada, Ada’s column fills up and the second statement becomes true as well.

The checkbox matters too. With “ignore $x = y$” turned off, the diagonal counts, and a celebrity would also have to follow themselves to fill their column. This is why careful translations often say “everyone else” and add the condition $x \ne y$, as you will see below.

One direction always works

The two statements are not equivalent, but they are not unrelated either. If there is a celebrity whom everyone follows, then certainly everyone follows someone, because they all follow the celebrity. In symbols:

while the converse fails, as the integer example and the network both show. A useful way to remember it: $\exists\forall$ is the strong, rare statement, and $\forall\exists$ is the weak, common one.

The four mixed and pure forms at a glance

For a predicate $P(x, y)$ of two variables, here is when each pattern is true and when it is false. It is worth reading slowly, one line at a time.

Statements from mathematics

Much of mathematics is written with nested quantifiers, often hidden behind ordinary words. Uncovering them is a good exercise in careful reading.

“The sum of two positive integers is always positive.” Two arbitrary integers are involved, and “always” means for all of them. With the domain of all integers:

“Every real number except zero has a multiplicative inverse.” For each nonzero $x$ we need some $y$ with $xy = 1$, and the $y$ clearly depends on $x$ (for 4 it is 0.25, for $-2$ it is $-0.5$):

This is true over the real numbers and false over the integers, where 2 has no integer inverse. Once again, the domain decides.

“There is no largest integer.” Saying that a largest integer exists would be $\exists y\, \forall x\; (x \le y)$. Its negation, as we will learn below, is $\forall y\, \exists x\; (x > y)$: whatever integer you name, there is a bigger one.

Translating English into logic

Translation with two quantifiers follows the same recipe as last week, with one extra habit: give each “thing” in the sentence its own variable, and decide for each variable whether the sentence means every one of them or some of them. Then the golden rule from week 4 applies to each quantifier separately: $\forall$ goes with $\to$, and $\exists$ goes with $\land$.

Let us work through several examples. In the first group the domain is all users of a messaging system, and $M(x, y)$ means “$x$ has sent a message to $y$”.

“Every user has sent a message to at least one other user.” “Every user” is the outer $\forall x$, “at least one other user” is an inner $\exists y$, and “other” means $y$ is not $x$ itself:

“There is a user who has sent messages to all other users.” Now the outer quantifier is $\exists x$, and “all other users” is a $\forall y$ restricted to $y \ne x$, so it takes an implication:

“There are two users who have sent messages to each other.”

“Some user has never received a message.” The user who receives is $y$, and “never” means from nobody:

The next examples use other domains. Read each sentence, decide on the variables, and only then look at the formula.

“Every student either has a computer or has a friend who has one.” With the domain all students in the school, $C(x)$: $x$ has a computer, and $F(x, y)$: $x$ and $y$ are friends:

“There is a woman who has taken a flight on every airline in the world.” Three kinds of things appear: women, flights and airlines. Let $P(w, f)$ mean that $w$ has taken flight $f$, and $Q(f, a)$ that flight $f$ belongs to airline $a$. The sentence names one woman, every airline, and for each airline some flight:

The flight is chosen after the airline, because it must be a flight of that airline. If you moved $\exists f$ to the front, you would claim that a single flight belongs to every airline, which is nonsense.

From logic back to English

Reading formulas aloud is just as important as writing them, and the goal is a sentence a person would actually say. Take $L(x, y)$: “$x$ loves $y$”, with the domain all people.

$\forall x\, \exists y\; L(x, y)$ says, word by word, “for every person $x$ there is a person $y$ such that $x$ loves $y$”, which is simply “everybody loves somebody.” The somebody may be different for each person.

$\exists y\, \forall x\; L(x, y)$ says “there is a person $y$ such that every person $x$ loves $y$”, that is, “there is someone whom everybody loves.” This is a much bolder claim, and the earlier result tells us it implies the first one.

$\forall x\, \forall y\; \big( L(x, y) \to L(y, x) \big)$ says that love is always returned: “if one person loves another, the other loves them back.” Unfortunately, a single counterexample from real life is enough to make it false.

Negating nested statements

To negate a nested statement, we use De Morgan’s laws for quantifiers from last week, one quantifier at a time, moving the negation from the outside inwards. Each time the negation passes a quantifier, that quantifier flips: $\forall$ becomes $\exists$ and $\exists$ becomes $\forall$. When the negation finally reaches the body, we simplify it with the laws from week 3.

The same procedure handles longer statements. Here are two from the practice slides, worked one step at a time. Try each one yourself before reading the solution.

Specifications: saying exactly what a program must do

Engineers use nested quantifiers every day, usually without calling them that, whenever they write down what a program is supposed to do. Such a description is called a specification. It usually has two parts: a precondition, which says what the program may assume about its input, and a postcondition, which says what must be true about its output when it finishes.

Take a function that sorts a list $a$ of length $n$ and returns a list $b$. What does “sorted correctly” actually mean? It means two things, and both need quantifiers.

The output must be in order. Every element is at most the next one:

And the output must contain the same elements as the input, nothing lost and nothing invented. A first attempt is to say that every value of $a$ appears somewhere in $b$:

This is a good start, but it is not quite enough. If $a = [3, 3, 1]$, the list $b = [1, 3, 5]$ is in order and contains every value of $a$, yet it is clearly wrong: one 3 is missing and a 5 appeared from nowhere. A complete specification must also say that each value occurs the same number of times in both lists. Finding such gaps is exactly the point of writing specifications precisely: a vague “the output is the sorted input” hides the question, while the formula forces you to face it.

The same ideas translate directly into tests:

def is_sorted(b):
    return all(b[i] <= b[i + 1] for i in range(len(b) - 1))                      # ∀i

def keeps_values(a, b):
    return all(any(a[i] == b[j] for j in range(len(b))) for i in range(len(a)))  # ∀i ∃j

def keeps_counts(a, b):
    return all(a.count(v) == b.count(v) for v in set(a) | set(b))                # ∀v

Many guarantees of real systems have the same shape. Here are a few, written with the obvious predicates.

Summary

A statement with nested quantifiers is read from the left, and each quantifier covers everything to its right. Two quantifiers of the same kind can be swapped freely, but a mixed pair cannot: $\forall x\, \exists y$ lets the choice of $y$ depend on $x$, while $\exists y\, \forall x$ demands one $y$ that works for every $x$. The second always implies the first, never the other way round. To decide which order a sentence needs, ask whether one choice depends on the other.

Over finite data, nested quantifiers are nested loops, and in Python they become nested calls to all and any. To negate a nested statement, move the negation inwards one quantifier at a time, flipping each quantifier it passes, and then simplify the body with the laws of logic. Finally, specifications are nested-quantifier statements about programs, and writing them precisely is one of the most practical skills this course offers.

Practice

Before the lab

In Lab 4 you will check nested-quantifier statements on a small social network: whether everyone follows someone, whether there is a celebrity, whether following is mutual. You will find witnesses and counterexamples with nested loops, and you will put the negation rule from this page into code.

Tags:nested quantifiersorder of quantifiersnegationspecificationpreconditionpostconditionε–δTLA+allany