🪴 GoDeep
Search
← Computer Science

Quantifiers: for all, there exists

How ∀ and ∃ turn open predicates into claims with truth values, and why the order you write them in changes the meaning.

14 cards · 8 quiz questions · 9 min read

“Users must have a valid email address.” Read that as a specification and a question appears immediately: all users, or some user? What counts as a user — every row in the table, or only the active ones? What if the table is empty? Ordinary English hides these questions. Quantifiers drag them into the open, which is exactly why every validation rule, database constraint and type checker you have ever written is quantified underneath.

From predicates to propositions

A proposition is a statement that already has a truth value: “7 is prime” is true, full stop. A predicate is a statement with a hole in it. Write P(x) for “x is prime” and you have something that is neither true nor false, because you have not said what x is. It is a function from values to truth values — in code, a function returning a boolean.

There are two ways to close the hole. You can substitute a value, giving P(7), which is true. Or you can quantify: say something about how many values in a collection satisfy the predicate. That is what quantifiers do, and there are two of them.

  • ∀ (for all), the universal quantifier. ∀x P(x) is true precisely when every x satisfies P, and false the instant one counterexample turns up.
  • ∃ (there exists), the existential quantifier. ∃x P(x) is true when at least one x satisfies P, and false only when every single one fails.

If those two feel familiar, they should:

const allPrime = xs.every(isPrime);  // ∀x ∈ xs, isPrime(x)
const anyPrime = xs.some(isPrime);   // ∃x ∈ xs, isPrime(x)

Python spells them all() and any(). SQL spells the existential one EXISTS. The notation is older than any of them, but it is the same idea.

The domain of discourse is part of the claim

∀x (x² ≥ 0) looks like an eternal truth. Over the real numbers it is one. Over the complex numbers it is false — take x = i, whose square is -1. The symbols did not change; the domain of discourse did. The domain is the set the variable ranges over, and a quantified statement has no truth value until you fix it.

This is not pedantry, it is the single most common source of ambiguous requirements. “Every order has a customer” over all orders is a different constraint from the same sentence over non-cancelled orders. When you write xs.every(...), xs is your domain of discourse, and picking the wrong array is picking the wrong claim.

Often you want to quantify over a big domain but restrict attention to part of it. The standard move is an implication inside the quantifier: “every prime greater than 2 is odd” becomes ∀x (Prime(x) ∧ x > 2 → Odd(x)). Because a conditional with a false antecedent counts as true, the statement is automatically satisfied by everything the restriction excludes — the same reason a check passes trivially on rows your WHERE clause filtered out.

Bound and free variables

In ∀x P(x, y), the quantifier binds x; y is left free. A formula with a free variable is still just a predicate, waiting for context. Only a closed formula, every variable bound, is true or false.

Bound variables behave exactly like a parameter name or a loop counter: they are private to their scope. ∀x P(x) and ∀y P(y) are the same statement, just as renaming a lambda’s argument changes nothing about what it computes. Free variables, by contrast, are captured from the surrounding environment, and their meaning depends on it.

Order changes everything

Here is the part that trips people up, and the reason quantifiers are worth learning properly. Let M(x, y) mean “y is the mother of x”, over the domain of all people.

  • ∀x ∃y M(x, y) — for every person, there is someone who is their mother. True.
  • ∃y ∀x M(x, y) — there is one person who is the mother of every person. False.

Same two quantifiers, same predicate, opposite truth values. The rule is about dependency: in ∀x ∃y, the choice of y is allowed to depend on x, so each x gets its own witness. In ∃y ∀x, y is chosen first and must work for everybody.

Adjacent quantifiers of the same kind commute freely: ∀x ∀y is ∀y ∀x, and ∃x ∃y is ∃y ∃x. Mixing ∀ with ∃ is where order becomes load-bearing.

The same trap appears in code review. “Every request has a handler that can serve it” and “there is one handler that can serve every request” describe very different architectures, and English lets you say both with almost the same words.

Negation: flip and push inwards

Two equivalences do most of the work in practice:

  • ¬∀x P(x) ≡ ∃x ¬P(x)
  • ¬∃x P(x) ≡ ∀x ¬P(x)

To deny that everything is prime is to claim something isn’t. To deny that anything is prime is to claim everything isn’t. The mechanical rule for a longer formula: push the negation inwards one step at a time, swapping each quantifier as it passes, until it lands on the predicate. So ¬∃x ∀y P(x, y) becomes ∀x ∃y ¬P(x, y).

This is precisely how you write a universal check in SQL, which has EXISTS but no ∀:

-- "every order in this batch has been paid"
-- rewritten as: no order in this batch is unpaid
SELECT NOT EXISTS (
  SELECT 1 FROM orders
  WHERE batch_id = 42 AND paid_at IS NULL
);

That query is ∀x P(x) ≡ ¬∃x ¬P(x) compiled into a database engine, and it is usually faster too — the search can stop at the first offending row.

Vacuous truth, and the empty array

What is ∀x P(x) worth when the domain is empty? It is true — vacuously true. A universal claim fails only by counterexample, and an empty domain has none to offer. Its mirror image: ∃x P(x) over an empty domain is false, because there is no witness.

Languages implement this faithfully, and it surprises people every time:

[].every(x => false);  // true
[].some(x => true);    // false
all([])  # True
any([])  # False

If your validator reports “all fields valid” on a form that parsed to zero fields, that is not a bug in the language. It is vacuous truth doing exactly what it says, and a reminder to check the domain before trusting the quantifier.

Sources

  • Kenneth H. Rosen — Discrete Mathematics and Its Applications book Chapter 1 develops predicates, quantifiers, nested quantifiers and their negations.
  • Daniel J. Velleman — How to Prove It: A Structured Approach book Careful treatment of free and bound variables and of quantifier order.
  • Stanford Encyclopedia of Philosophy — The Logic of Quantifiers website Background on quantification and the domain of discourse.
  • Jon Barwise & John Etchemendy — Language, Proof and Logic book Introductory first-order logic with an emphasis on translating English into quantified sentences.