Set-builder notation, quantifiers and infinite sets

A transport official in Kampala announces: “Every bus on Route 7 arrived on time today.” Nadia waited twenty minutes for hers. What exactly does she need to show to prove the announcement false? Not that no bus was on time — just that at least one bus was late.

Now compare two sentences about a village:

• “Everyone in the village has someone they can ask for help.”
• “There is someone in the village whom everyone can ask for help.”

They use the same words, in a different order, and say very different things. The first could be true because neighbours help each other; the second needs one remarkable person.

And here is a bigger question: how many natural numbers are there? “Infinitely many,” you might say. But what does that mean — and how could anyone be sure, without checking them all?

This lesson gives you the precise language for all three questions: sets described by rules, the words for all and there exists, and infinite sets.

A set can be given by a list of its elements, like $\{2, 4, 6\}$, or by a rule that says which elements belong. Think of a door with a doorkeeper: you name the crowd waiting outside (“the natural numbers”), and the doorkeeper lets in exactly those who pass a test (“is even”). Rules can describe sets far too large to list, such as all the even numbers.

Statements about all members and some members of a set behave like checks and searches:

• “Every element has the property” is a check: it is true only if every single element passes. One failure makes it false.
• “Some element has the property” is a search: it is true as soon as one element passes. It is false only if every element fails.

On a small set such as $\{1, 2, 3\}$, “every element has property $P$” just means “$P(1)$ and $P(2)$ and $P(3)$”, while “some element has $P$” means “$P(1)$ or $P(2)$ or $P(3)$”. Denying a long “and” gives a long “or” of denials — which is exactly why one late bus is enough.

Throughout, $\N = \{0, 1, 2, 3, \dots\}$ is the set of natural numbers and $\Z$ the set of integers.

A second form describes a set by a formula for its elements: $\{\, 2k : k \in \N \,\}$ is the set of all numbers $2k$ with $k$ a natural number, that is $\{0, 2, 4, 6, \dots\}$.

The letter in set-builder notation is a placeholder: $\{x \in \N : x < 3\}$ and $\{n \in \N : n < 3\}$ are the same set, $\{0, 1, 2\}$.

“There exists” means at least one, not exactly one: $\exists n \in \N,\ n > 5$ is true, with many witnesses. On its own, a statement such as “$x > 5$” is neither true nor false — it becomes true or false once we say what $x$ is, or quantify it.

In this section $A$ is any set and $P(x)$ any statement about elements of $A$.

The last step used the principle that “not failing $P$” means “having $P$”. Every statement is either true or false — the law of excluded middle. Almost all of mathematics uses it freely; the logic viewpoint below explains who doesn't, and why.

In the first statement $y$ may depend on $x$ (we chose $y = x + 1$). In the second, one single $y$ must work for every $x$ at once. In general, “$\exists y\ \forall x$” implies “$\forall x\ \exists y$” — the one $y$ that works for everybody works for each $x$ — but not the other way round.

So “every element of the empty set is even” and “every element of the empty set is odd” are both true. They do not contradict each other, because there is nothing that would have to be even and odd at once.

Look at the quantifiers: for every list there exists a missing number, and the missing number depends on the list. The swapped statement — “there is a number missing from every finite list” — is false, because whatever number $m$ you pick, the one-item list $m$ contains it.

Lean's logic is made of exactly these quantifiers: ∀ x, P x and ∃ x, P x. A set described by a rule is represented by the rule itself — a property of natural numbers:

/-- The set `{n ∈ ℕ | n is even}`, written as a predicate: `Evens n` is the statement that `n`
leaves remainder `0` on division by `2`. -/
def Evens (n : Nat) : Prop := n % 2 = 0

/-- Membership is checked by evaluating the property: `10` is in the set, `7` is not. -/
theorem evens_examples : Evens 10 ∧ ¬ Evens 7 := by
  unfold Evens
  decide

Two set-builder descriptions give the same set when membership in one is equivalent to membership in the other (↔, “if and only if”):

/-- Two set-builder descriptions of the same set: `{n ∈ ℕ | n is even} = {2k | k ∈ ℕ}`.
A number is even exactly when it is `2k` for some natural number `k`. -/
theorem evens_iff_double (n : Nat) : Evens n ↔ ∃ k, n = 2 * k := by
  unfold Evens
  constructor
  · intro h
    exact ⟨n / 2, by omega⟩
  · intro ⟨k, hk⟩
    omega

/-- `{n ∈ ℕ | n² < 20} = {0, 1, 2, 3, 4}`: a natural number has square below `20` exactly when it
is at most `4`. If `n ≥ 5` then `n · n ≥ 5 · 5 = 25`; if `n ≤ 4` then `n · n ≤ 4 · 4 = 16`. -/
theorem small_squares (n : Nat) : n * n < 20 ↔ n ≤ 4 := by
  constructor
  · intro h
    apply Nat.le_of_not_lt
    intro h5
    have : 5 * 5 ≤ n * n := Nat.mul_le_mul h5 h5
    omega
  · intro h
    have : n * n ≤ 4 * 4 := Nat.mul_le_mul h h
    omega

The negation rules of Theorem 1, proved step by step. Notice Classical.byContradiction in the first proof: that is the law of excluded middle at work, exactly where the human proof used it.

/-- **"Not every `x` has `P`" means "some `x` does not have `P`".**
(←) If `x` fails `P`, then not every element has `P`.
(→) By contradiction: if *no* `x` failed `P`, then every `x` would have `P` — again by
contradiction — which we were told is false. This direction uses classical logic
(`Classical.byContradiction`, a form of the law of excluded middle). -/
theorem not_forall_iff {α : Type} (P : α → Prop) : (¬ ∀ x, P x) ↔ ∃ x, ¬ P x := by
  constructor
  · intro h
    apply Classical.byContradiction
    intro hnone
    apply h
    intro x
    apply Classical.byContradiction
    intro hx
    exact hnone ⟨x, hx⟩
  · intro ⟨x, hx⟩ hall
    exact hx (hall x)

/-- **"No `x` has `P`" means "every `x` fails `P`".** Both directions are direct: an `x` with
`P x` would contradict "every `x` fails `P`", and vice versa. (Core Lean: `not_exists`.) -/
theorem not_exists_iff {α : Type} (P : α → Prop) : (¬ ∃ x, P x) ↔ ∀ x, ¬ P x := by
  constructor
  · intro h x hx
    exact h ⟨x, hx⟩
  · intro h ⟨x, hx⟩
    exact h x hx

Core Lean also has the first rule in its library; this version just applies it:

/-- The same law, applying core Lean's `Classical.not_forall`. -/
theorem not_forall_library {α : Type} (P : α → Prop) : (¬ ∀ x, P x) ↔ ∃ x, ¬ P x :=
  Classical.not_forall

Applying the two rules one after another negates a statement with two quantifiers:

/-- Negating a statement with two quantifiers: apply the two rules one after the other.
`¬ (∀ x, ∃ y, R x y)` becomes `∃ x, ¬ ∃ y, R x y`, which becomes `∃ x, ∀ y, ¬ R x y`. -/
theorem not_forall_exists {α β : Type} (R : α → β → Prop) :
    (¬ ∀ x, ∃ y, R x y) ↔ ∃ x, ∀ y, ¬ R x y := by
  rw [not_forall_iff]
  constructor
  · intro ⟨x, hx⟩
    exact ⟨x, (not_exists_iff (R x)).mp hx⟩
  · intro ⟨x, hx⟩
    exact ⟨x, (not_exists_iff (R x)).mpr hx⟩

/-- In ℕ, **for every `x` there is a `y` with `y > x`**: given `x`, take `y = x + 1`.
Notice that `y` is allowed to depend on `x`. -/
theorem forall_exists_gt : ∀ x : Nat, ∃ y, y > x :=
  fun x => ⟨x + 1, Nat.lt_succ_self x⟩

/-- In ℕ, **there is no `y` with `y > x` for every `x`**: such a `y` would have to be bigger
than itself. Same symbols as `forall_exists_gt`, different order — and the opposite answer. -/
theorem not_exists_forall_gt : ¬ ∃ y : Nat, ∀ x, y > x := by
  intro ⟨y, hy⟩
  exact Nat.lt_irrefl y (hy y)

/-- In ℤ, every number has a partner that adds to zero: `∀ x, ∃ y, x + y = 0` (take `y = -x`). -/
theorem int_forall_exists : ∀ x : Int, ∃ y, x + y = 0 :=
  fun x => ⟨-x, by omega⟩

/-- But no single number is a partner for *every* `x`: `¬ ∃ y, ∀ x, x + y = 0`. Taking `x = 0`
forces `y = 0`, and then `x = 1` gives `1 = 0`. -/
theorem int_not_exists_forall : ¬ ∃ y : Int, ∀ x : Int, x + y = 0 := by
  intro ⟨y, hy⟩
  have h0 := hy 0
  have h1 := hy 1
  omega

Vacuous truth, as Lean sees it: to prove something about every element of the empty list, you are handed an element of the empty list — and that is already impossible.

/-- **Vacuous truth.** "Every element of the empty list is even" is true — and so is "every
element of the empty list is odd". There is no element to check, so there is no counterexample. -/
theorem vacuous_empty_list :
    (∀ n, n ∈ ([] : List Nat) → Evens n) ∧ (∀ n, n ∈ ([] : List Nat) → ¬ Evens n) := by
  constructor
  · intro n h
    exact absurd h (List.not_mem_nil)
  · intro n h
    exact absurd h (List.not_mem_nil)

/-- "Every natural number less than `0` equals `42`" is (vacuously) true: no natural number is
less than `0`. -/
theorem vacuous_below_zero : ∀ n : Nat, n < 0 → n = 42 := by
  intro n h
  omega

Checking cases is not the same as proving “for all”. On a finite range, Lean's decide simply runs through the cases. For all of $\N$ we need an argument that reduces infinitely many cases to finitely many — here, the four possible remainders on division by $4$:

/-- For each of the `50` numbers `n < 50`, `n²` leaves remainder `0` or `1` on division by `4`.
`decide` proves this by checking all fifty cases — a proof about these fifty numbers only. -/
theorem squares_mod_four_check : ∀ n, n < 50 → n * n % 4 = 0 ∨ n * n % 4 = 1 := by
  decide

/-- The same fact for **every** natural number. No computer can check infinitely many cases, but
an argument can: the remainder of `n · n` on division by `4` depends only on the remainder `r` of
`n` (`Nat.mul_mod`), and there are only four possible remainders `r = 0, 1, 2, 3`. -/
theorem squares_mod_four (n : Nat) : n * n % 4 = 0 ∨ n * n % 4 = 1 := by
  have four_cases : ∀ r, r < 4 → r * r % 4 = 0 ∨ r * r % 4 = 1 := by decide
  rw [Nat.mul_mod]
  exact four_cases (n % 4) (Nat.mod_lt n (by decide))

Finally, Theorems 4 and 5. A finite list's largest number is computed by a small program, listMax; a proof by induction on the list shows that every entry is at most listMax; and then listMax + 1 cannot be on the list.

/-- The largest number in a finite list of natural numbers (`0` for the empty list). -/
def listMax : List Nat → Nat
  | [] => 0
  | x :: xs => max x (listMax xs)

/-- Every number in a list is at most `listMax` of the list. Proof by induction on the list:
the head is at most `max head rest`, and every element of the tail is at most `listMax tail`,
which is at most `max head (listMax tail)`. -/
theorem le_listMax : ∀ (l : List Nat) (x : Nat), x ∈ l → x ≤ listMax l
  | [], x, h => absurd h List.not_mem_nil
  | y :: ys, x, h => by
    cases h with
    | head => exact Nat.le_max_left _ _
    | tail _ h' => exact Nat.le_trans (le_listMax ys x h') (Nat.le_max_right y (listMax ys))

/-- **ℕ is infinite**: for every finite list of natural numbers, one more than its largest
number is missing from it. (If `listMax l + 1` were in the list, it would be at most
`listMax l`.) -/
theorem nat_infinite (l : List Nat) : listMax l + 1 ∉ l := by
  intro h
  have := le_listMax l (listMax l + 1) h
  omega

/-- So no finite list contains every natural number. -/
theorem no_list_of_all_nats : ¬ ∃ l : List Nat, ∀ n, n ∈ l := by
  intro ⟨l, hl⟩
  exact nat_infinite l (hl (listMax l + 1))

/-- **The even numbers are infinite too**: for every finite list, `2 · (largest + 1)` is even,
bigger than every number in the list, and therefore missing from it. -/
theorem evens_infinite (l : List Nat) : ∃ n, Evens n ∧ n ∉ l := by
  refine ⟨2 * (listMax l + 1), ?_, ?_⟩
  · unfold Evens
    omega
  · intro h
    have := le_listMax l (2 * (listMax l + 1)) h
    omega

What is formalised: every theorem of the proof section, using core Lean only (for an empty list, Lean's listMax is $0$, so the missing number it produces is $1$ rather than $0$ — either works). Mathlib, Lean's large mathematical library, has the general notions: Set.Infinite, Set.Finite, and the theorem Set.infinite_of_not_bddAbove, which says that a set of natural numbers with no upper bound is infinite.

"""For all and there exists, on finite sets: Python's all() and any().

On a finite set, "for every x, P(x)" is a long AND and "there is an x with
P(x)" is a long OR - exactly Python's all() and any(). The experiment checks
the negation rules for every predicate on every universe with at most five
elements, shows vacuous truth (all([]) is True), and shows that the order of
mixed quantifiers changes the answer. It also shows why a finite check cannot
settle a statement about all of N: cutting N off at 9 makes "for every x
there is a bigger y" false. Exhaustive-finite evidence only.
"""

import itertools

def forall(universe, pred):
    """'For every x in universe, pred(x)' on a finite universe."""
    return all(pred(x) for x in universe)

def exists(universe, pred):
    """'There is an x in universe with pred(x)' on a finite universe."""
    return any(pred(x) for x in universe)

def forall_exists(xs, ys, rel):
    """'For every x there is a y with rel(x, y)' (y may depend on x)."""
    return all(any(rel(x, y) for y in ys) for x in xs)

def exists_forall(xs, ys, rel):
    """'There is a y with rel(x, y) for every x' (one y for all x)."""
    return any(all(rel(x, y) for x in xs) for y in ys)

def predicates(universe):
    """Every predicate on a finite universe, as a set of the true elements."""
    items = list(universe)
    for r in range(len(items) + 1):
        for chosen in itertools.combinations(items, r):
            yield frozenset(chosen)

def negation_rules_hold(universe):
    """Count predicates for which both negation rules agree, and the total."""
    agree = total = 0
    for truth in predicates(universe):
        p = truth.__contains__
        rule1 = (not forall(universe, p)) == exists(universe, lambda x: not p(x))
        rule2 = (not exists(universe, p)) == forall(universe, lambda x: not p(x))
        agree += rule1 and rule2
        total += 1
    return agree, total

def main():
    nums = range(100)
    print("1. Quantifiers over the finite set {0, ..., 99}")
    print("   every n has n*n % 4 in {0, 1}:   ",
          forall(nums, lambda n: n * n % 4 in (0, 1)))
    print("   some n has n*n % 4 == 2:         ",
          exists(nums, lambda n: n * n % 4 == 2))
    print()
    print("2. Negation rules, every predicate on universes of size 0..5")
    agree = total = 0
    for size in range(6):
        a, t = negation_rules_hold(range(size))
        agree, total = agree + a, total + t
    print(f"   not-all == some-not and not-some == all-not: {agree}/{total}")
    print()
    print("3. Vacuous truth: statements about the elements of the empty set")
    print("   all([]) =", all([]), "  any([]) =", any([]))
    print("   every element of {} is even:", forall([], lambda n: n % 2 == 0))
    print("   every element of {} is odd: ", forall([], lambda n: n % 2 == 1))
    print()
    print("4. The order of quantifiers")
    zs = range(-5, 6)
    add0 = lambda x, y: x + y == 0  # noqa: E731
    print("   on {-5..5}, for all x some y has x + y = 0:",
          forall_exists(zs, zs, add0))
    print("   on {-5..5}, some y has x + y = 0 for all x:",
          exists_forall(zs, zs, add0))
    cut = range(10)
    bigger = lambda x, y: y > x  # noqa: E731
    print("   on {0..9}, for all x some y > x:", forall_exists(cut, cut, bigger))
    print("   on {0..9}, some y >= every x:   ",
          exists_forall(cut, cut, lambda x, y: y >= x))
    print("   In N the answers flip: every x has a bigger y, and no y is >=")
    print("   every x. A finite piece of N has a largest element; N has not.")
    print()
    print("Epistemic status: exact, exhaustive checks on finite sets. Part 2")
    print("checks the negation rules for the 63 predicates on universes of up")
    print("to 5 elements; the lesson proves them for every set. Part 4 shows a")
    print("finite check of a statement about all of N can give the wrong answer.")

if __name__ == "__main__":
    main()

Part 4 holds a warning. On the finite set $\{0, \dots, 9\}$, “for every $x$ there is a bigger $y$” is false (nothing is bigger than $9$), and “some $y$ is at least every $x$” is true ($y = 9$). In $\N$ both answers flip. So no finite check can settle a statement about all natural numbers — for that we need a proof like Theorem 2.

"""Set-builder notation as Python set comprehensions, and why N is infinite.

{n in A : P(n)} becomes {n for n in A if P(n)}, and {2k : k in A} becomes
{2 * k for k in A}. The experiment checks that two descriptions of the even
numbers agree on a finite range, lists a few small sets, then plays the
"infinite set" game: whatever finite list of natural numbers you give, one
more than its largest element is missing, and twice that is a missing even
number. Exact computation on finite ranges and sample lists; the lesson
proves the general statements.
"""

def evens_by_property(limit):
    """{n in {0..limit-1} : n is even}."""
    return {n for n in range(limit) if n % 2 == 0}

def evens_by_formula(limit):
    """{2k : k in N, 2k < limit}."""
    return {2 * k for k in range((limit + 1) // 2)}

def small_squares():
    """{x in Z : x * x < 10}. Searching -10..10 is enough, because
    |x| >= 4 gives x * x >= 16."""
    return sorted(x for x in range(-10, 11) if x * x < 10)

def primes_below(n):
    """{p in N : p is prime and p < n}."""
    return [p for p in range(2, n) if all(p % d for d in range(2, p))]

def missing_natural(numbers):
    """A natural number not in the finite list: one more than the largest."""
    return max(numbers, default=-1) + 1

def missing_even(numbers):
    """An even natural number not in the finite list."""
    return 2 * (max(numbers, default=-1) + 1)

def main():
    print("1. Set-builder notation as set comprehensions")
    same = evens_by_property(1000) == evens_by_formula(1000)
    print("   {n < 1000 : n even} == {2k : 2k < 1000}:", same)
    print("   {x in Z : x*x < 10} =", small_squares())
    print("   {p prime : p < 30} =", primes_below(30))
    print("   {n in 0..99 : n < 0} =", {n for n in range(100) if n < 0},
          "(the empty set)")
    print()
    print("2. No finite list contains every natural number")
    lists = [[], [0, 1, 2, 3], [7, 3, 12], [2, 4, 6, 8, 10, 12],
             [5, 10 ** 6, 41]]
    for nums in lists:
        n, e = missing_natural(nums), missing_even(nums)
        assert n not in nums and e not in nums and e % 2 == 0
        print(f"   {str(nums):<22} misses {n:>7} and the even number {e:>7}")
    print("   Whatever finite list you write, the recipe finds a number it")
    print("   misses - so N and the even numbers are infinite.")
    print()
    print("Epistemic status: exact computations. Part 1 compares two")
    print("descriptions only on 0..999, and part 2 tries five lists; neither")
    print("is a proof about all numbers. The lesson proves that largest + 1")
    print("is missing from every finite list (and Lean checks the proof).")

if __name__ == "__main__":
    main()

Take the three-element set $\{1, 2, 3\}$ and a property $P$. Let $p$, $q$ and $r$ stand for the statements $P(1)$, $P(2)$ and $P(3)$. Then “every element has $P$” is $p \wedge q \wedge r$ (“and”), and “some element fails $P$” is $\neg p \vee \neg q \vee \neg r$ (“or”). Theorem 1(a) predicts that denying the first gives the second. The truth table checks all eight possible properties at once:

And Theorem 1(b): “no element has $P$” against “every element fails $P$”.

Things to try: the two columns agree in every row, so each pair is a logical equivalence (these are De Morgan's laws). Now replace not p or not q or not r by the tempting wrong denial not p and not q and not r (“every element fails”) in the first table, and find a row where it disagrees with not (p and q and r).

• Aristotle (Athens, 4th century BCE) studied the four forms “every A is B”, “no A is B”, “some A is B” and “some A is not B”, and how they deny one another — later drawn as the square of opposition.
• Euclid's Elements (around 300 BCE) states that “prime numbers are more than any assigned multitude of prime numbers” (Book IX, Proposition 20) — a statement about every finite list, proved exactly in the style of Theorem 4.
• Jaina mathematicians in ancient India classified numbers as enumerable, innumerable and infinite, and distinguished several kinds of infinity (described in G. G. Joseph's The Crest of the Peacock).
• Galileo Galilei, in Two New Sciences (1638), noticed that the perfect squares can be paired off with all the natural numbers, although most numbers are not squares — a puzzle about infinite sets that Georg Cantor resolved in the 1870s–1890s by taking such pairings as the definition of “same size” (see countability).
• Quantifiers as symbols came with modern logic: Gottlob Frege's Begriffsschrift (1879) and, independently, Charles Sanders Peirce (1885). The symbol $\exists$ was introduced by Giuseppe Peano (1897), and $\forall$ by Gerhard Gentzen (1935).

• Daniel J. Velleman, How to Prove It: A Structured Approach (3rd edition, 2019), chapter 2 on quantificational logic and set-builder notation.
• Richard Hammack, Book of Proof (3rd edition, 2018), chapters 1 and 2 on sets and logic — free to read online.
• Eli Maor, To Infinity and Beyond: A Cultural History of the Infinite (1987).
• Hans Magnus Enzensberger, The Number Devil (1997) — a story for young readers, with infinitely many numbers in it.