Countability and Cantor's diagonal argument

Lens

MotivationH

The hotel with infinitely many rooms

Imagine a hotel with rooms numbered $0, 1, 2, 3, \dots$ — one for every natural number — and every room is occupied. A traveller arrives. Is there room?

Yes: ask every guest to move from room $n$ to room $n + 1$ . Room $0$ is now free. Now a coach arrives with infinitely many travellers, numbered $0, 1, 2, \dots$ Still no problem: move each guest from room $n$ to room $2n$ , freeing all the odd-numbered rooms, and put traveller $k$ in room $2k + 1$ .

This thought experiment is usually credited to David Hilbert, in a lecture of 1924, and was made famous by George Gamow's book One Two Three… Infinity (1947). It raises a serious question: is every infinite crowd the same size? Could any infinite collection of travellers be fitted into the hotel? In this lesson we shall see that the answer is no — and prove it with one of the most beautiful arguments in mathematics.

IntuitionH

Counting is matching

Long before anyone wrote numerals, a herder could check that every animal had come home by matching animals with pebbles in a bag. Two collections have the same size when their members can be paired off perfectly, with nothing left over on either side. Counting a finite set is just matching it with $\{1, 2, \dots, n\}$ .

For infinite sets, matching gives surprises. In 1638 Galileo Galilei noticed that the squares $1, 4, 9, 16, \dots$ can be matched with all the counting numbers $1, 2, 3, 4, \dots$ by $n \leftrightarrow n^2$ — even though most counting numbers are not squares. Galileo concluded that "equal", "greater" and "less" do not apply to infinite quantities. Two and a half centuries later Georg Cantor made the opposite, bold choice: define "same size" by perfect matching, and accept that a part can be as large as the whole. The rest of this lesson follows Cantor.

DefinitionsH

Definitions

We use $\N = \{0, 1, 2, \dots\}$ and the language of functions: injective, surjective, bijective.

Definition— same cardinality

Sets $A$ and $B$ have the same cardinality, written $|A| = |B|$ , if there is a bijection $A \to B$ . We write $|A| \le |B|$ if there is an injection $A \to B$ , and $|A| < |B|$ if $|A| \le |B|$ but $|A| \ne |B|$ .

Definition— countable, uncountable

A set is countably infinite if it has the same cardinality as $\N$ , and countable if it is finite or countably infinite. A set that is not countable is uncountable.

A countably infinite set is one whose elements can be arranged in an infinite list $a_0, a_1, a_2, \dots$ in which every element appears exactly once. It is often easier to allow repetitions:

Theorem— Lemma 1 (lists with repetitions are enough)

(a) Every subset of $\N$ is countable. (b) If there is an injection $A \to \N$ , then $A$ is countable. (c) If $A$ is non-empty and there is a surjection $\N \to A$ — a list $a_0, a_1, a_2, \dots$ in which every element of $A$ appears at least once — then $A$ is countable.

Proof

(a) Let $S \subseteq \N$ be infinite. By the well-ordering principle, let $s_0$ be its least element, $s_1$ the least element of $S \setminus \{s_0\}$ , and so on. Then $k \mapsto s_k$ is injective (the $s_k$ increase), and surjective: an element $s \in S$ has only finitely many elements of $S$ below it, say $j$ of them, and then $s = s_j$ . (b) An injection $f : A \to \N$ is a bijection from $A$ onto the subset $f(A)$ , which is countable by (a). (c) Send each $a \in A$ to the least $n$ with $a_n = a$ . Different elements get different numbers, so this is an injection $A \to \N$ , and (b) applies.

∎

Definition— power set

The power set $\mathcal{P}(A)$ of a set $A$ is the set of all subsets of $A$ . For example $\mathcal{P}(\{0, 1\}) = \{\varnothing, \{0\}, \{1\}, \{0, 1\}\}$ . A finite set with $n$ elements has $2^n$ subsets.

ProofH

Sets that can be listed

Theorem— Theorem 2 (a part as large as the whole)

The set $E = \{0, 2, 4, \dots\}$ of even natural numbers has the same cardinality as $\N$ .

Proof

The function $n \mapsto 2n$ from $\N$ to $E$ is injective ( $2m = 2n$ implies $m = n$ ) and surjective (every even number is $2n$ for some $n$ ).

∎

Theorem— Theorem 3 (the integers are countable)

The function $z : \N \to \Z$ given by

z(n) = \begin{cases} n/2 & \text{if } n \text{ is even,} \\ -(n + 1)/2 & \text{if } n \text{ is odd,} \end{cases}

is a bijection. It lists the integers as $0, -1, 1, -2, 2, -3, 3, \dots$

Proof

Injective. Even inputs give values $\ge 0$ and odd inputs give values $\le -1$ , so two inputs with the same value have the same parity. If both are even, $m/2 = n/2$ gives $m = n$ ; if both are odd, $-(m+1)/2 = -(n+1)/2$ gives $m = n$ . Surjective. An integer $k \ge 0$ equals $z(2k)$ , and an integer $k \le -1$ equals $z(-2k - 1)$ , where $-2k - 1 \ge 1$ is odd.

∎

Theorem— Theorem 4 (pairs of natural numbers are countable)

Cantor's pairing function $\pi : \N \times \N \to \N$ ,

\pi(m, n) = \frac{(m + n)(m + n + 1)}{2} + n,

is a bijection. Hence $|\N \times \N| = |\N|$ .

Cantor's pairing walks the grid of pairs (m, n) diagonal by diagonal. The diagonal m + n = d holds d + 1 points, so the walk reaches every pair, each exactly once.

Proof

Write $T(d) = 0 + 1 + \dots + d = d(d + 1)/2$ . The pair $(m, n)$ lies on the diagonal $d = m + n$ , and $\pi(m, n) = T(d) + n$ with $0 \le n \le d$ . So the values on diagonal $d$ are exactly the $d + 1$ numbers $T(d), T(d) + 1, \dots, T(d) + d$ , and the next diagonal starts at $T(d + 1) = T(d) + d + 1$ .

Injective. If $\pi(m, n) = \pi(m', n')$ with $d = m + n < d' = m' + n'$ , then $\pi(m, n) \le T(d) + d < T(d + 1) \le T(d') \le \pi(m', n')$ , which is impossible. So $d = d'$ ; then $T(d) + n = T(d) + n'$ gives $n = n'$ , and $m = d - n = m'$ . Surjective. The blocks $\{T(d), \dots, T(d) + d\}$ for $d = 0, 1, 2, \dots$ fit together without gaps and cover all of $\N$ , so every $k \in \N$ lies in one of them: $k = T(d) + n$ with $0 \le n \le d$ , which is $\pi(d - n, n)$ .

∎

Theorem— Theorem 5 (the rationals are countable)

$\Q$ is countable.

Proof

Every rational number can be written $a/b$ with $a \in \Z$ and $b \in \{1, 2, 3, \dots\}$ . Define a list of rationals by $q_k = z(m)/(n + 1)$ , where $(m, n)$ is the pair with $\pi(m, n) = k$ (Theorem 4) and $z$ is the zigzag of Theorem 3. Given $a/b$ , choose $m$ with $z(m) = a$ and let $n = b - 1$ ; then $a/b = q_{\pi(m, n)}$ . So every rational appears in the list (many times, since $1/2 = 2/4 = \cdots$ ), and $\Q$ is countable by Lemma 1(c).

∎

There is even a list of the positive rationals with no repetitions and no cancelling: the Calkin–Wilf sequence $1, \tfrac12, 2, \tfrac13, \tfrac32, \tfrac23, 3, \tfrac14, \dots$ , in which each term $x$ is followed by $1/(2\lfloor x \rfloor - x + 1)$ (Neil Calkin and Herbert Wilf, 2000; the formula is due to Moshe Newman). The computation section runs it.

Theorem— Theorem 6 (countable unions)

If $A_0, A_1, A_2, \dots$ are countable sets, then their union $\bigcup_i A_i$ is countable.

Proof

We may assume each $A_i$ is non-empty (empty ones contribute nothing; if all are empty the union is empty). For each $i$ choose a list $f_i(0), f_i(1), \dots$ of $A_i$ in which every element appears (Lemma 1, allowing repetitions; a finite set can be listed by repeating its last element). Then $k \mapsto f_m(n)$ , where $\pi(m, n) = k$ , is a list in which every element of every $A_i$ appears. By Lemma 1(c) the union is countable.

∎

Note

The proof chooses a list for each of infinitely many sets at once. In axiomatic set theory this needs (a weak form of) the axiom of choice — see the axiom of choice. When the lists are given explicitly, as in all our examples, no choice is needed.

A consequence: the algebraic numbers — real numbers that are roots of non-zero polynomials with integer coefficients, such as $\sqrt{2}$ , $\sqrt[3]{5}$ and $\tfrac12(1 + \sqrt{5})$ — form a countable set. There are countably many polynomials of each degree (their coefficient lists form a countable set, by Theorem 4 applied repeatedly), each has finitely many roots, and Theorem 6 collects them all.

ProofH

Sets that cannot be listed

Theorem— Theorem 7 (Cantor's theorem)

For every set $A$ , there is no surjection $f : A \to \mathcal{P}(A)$ . Consequently $|A| < |\mathcal{P}(A)|$ .

Proof

Let $f : A \to \mathcal{P}(A)$ be any function. Consider the diagonal set

D = \{a \in A : a \notin f(a)\} \subseteq A .

Suppose $D = f(d)$ for some $d \in A$ . If $d \in D$ , then by the definition of $D$ , $d \notin f(d) = D$ . If $d \notin D$ , then $d \notin f(d)$ , so by the definition of $D$ , $d \in D$ . Both cases are impossible, so $D$ is not a value of $f$ , and $f$ is not surjective. Finally, $a \mapsto \{a\}$ is an injection $A \to \mathcal{P}(A)$ , so $|A| \le |\mathcal{P}(A)|$ ; since there is no bijection, $|A| < |\mathcal{P}(A)|$ .

∎

So there is no largest infinity: $|\N| < |\mathcal{P}(\N)| < |\mathcal{P}(\mathcal{P}(\N))| < \cdots$ . For a finite set the theorem says $n < 2^n$ ; for $\N$ it says the subsets of $\N$ cannot be listed.

A subset $S \subseteq \N$ is the same thing as an infinite sequence of 0s and 1s (put $1$ in position $n$ exactly when $n \in S$ ). In that language Cantor's proof is the famous diagonal argument:

Theorem— Theorem 8 (0–1 sequences)

The set of infinite sequences of 0s and 1s is uncountable.

Proof

Given any list $s_0, s_1, s_2, \dots$ of such sequences, define a sequence $d$ by making its $n$ -th entry the opposite of the $n$ -th entry of $s_n$ . Then $d$ differs from $s_0$ in entry $0$ , from $s_1$ in entry $1$ , and in general from $s_n$ in entry $n$ . So $d$ is not on the list. Since every list misses a sequence, the set is uncountable.

∎

Theorem— Theorem 9 (the real numbers are uncountable)

The interval $[0, 1)$ , and hence $\R$ , is uncountable.

We use two facts about decimals (see real numbers): every $x \in [0, 1)$ has a decimal expansion $0.d_1 d_2 d_3 \dots$ that does not end in an infinite run of 9s, and two different expansions of this kind name different numbers. (The only way one number can have two expansions is like $0.5000\dots = 0.4999\dots$ )

Proof

Suppose $r_1, r_2, r_3, \dots$ were a list of all numbers in $[0, 1)$ . Write each in its expansion without a tail of 9s, $r_n = 0.d_{n1} d_{n2} d_{n3} \dots$ Define $x = 0.e_1 e_2 e_3 \dots$ by

e_n = \begin{cases} 4 & \text{if } d_{nn} = 5, \\ 5 & \text{otherwise.} \end{cases}

The digits of $x$ are all 4s and 5s, so this is an expansion without a tail of 9s, and $x \in [0, 1)$ . It differs from the expansion of $r_n$ in the $n$ -th digit, so by the second fact $x \neq r_n$ — for every $n$ . So $x$ is not on the list, a contradiction. Since $[0, 1) \subseteq \R$ and a subset of a countable set is countable (compose the inclusion with an injection into $\N$ and use Lemma 1(b)), $\R$ is uncountable too.

∎

Choosing the digits 4 and 5 is not fussiness: a careless rule could produce $x = 0.4999\dots$ , which is the listed number $0.5$ in disguise (the computation section builds exactly this trap).

Theorem— Corollary 10 (Cantor, 1874)

Transcendental numbers exist: some real numbers are not roots of any non-zero polynomial with integer coefficients. Indeed, all but countably many real numbers are transcendental.

Proof

The algebraic numbers form a countable set (end of the previous section), and $\R$ is uncountable. So $\R$ is not equal to the set of algebraic numbers; in fact removing a countable set from $\R$ leaves an uncountable set, since the union of two countable sets is countable.

∎

This proof does not exhibit a single transcendental number! Explicit ones had been found by Joseph Liouville in 1844, such as $\sum_{n \ge 1} 10^{-n!} = 0.110001000\dots$ ; Charles Hermite proved $e$ transcendental in 1873 and Ferdinand von Lindemann proved the same for $\pi$ in 1882.

How big is $\R$ ? In fact $|\R| = |\mathcal{P}(\N)|$ : binary expansions give an injection $[0, 1) \to \mathcal{P}(\N)$ , decimal expansions using only the digits 0 and 1 give an injection back, and the Schröder–Bernstein theorem (see ordinals and cardinals) turns two injections into a bijection. Is there a set strictly larger than $\N$ but strictly smaller than $\R$ ? Cantor conjectured not — the continuum hypothesis. Kurt Gödel (1940) and Paul Cohen (1963) showed that, if the standard axioms of set theory (ZFC) are consistent, they can neither prove nor refute it; see forcing and independence.

Explore

Explore: the diagonal machine

Each row is the start of an infinite 0–1 sequence. Click any digit to change the list — and watch the gold sequence $d$ change so that it still differs from every row.

The diagonal machine

Here is a list of infinite 0–1 sequences (we can only show the start). The gold sequence d flips the diagonal.

s1											…
s2											…
s3											…
s4											…
s5											…
s6											…

d	1	0	1	0	0	1	?	?	?	?	…

Point at (or tab to) a row to see where d differs from it. Click any digit to change the list.

Add d to the list and a new d appears that is different again. No list — however long — can contain every sequence.

Things to try:

Make the list "cleverer": change row 1 so that it equals the current $d$ . What happens to $d$ ?
Add rows. Is there ever a list where $d$ appears as one of the rows? Why not, whatever you do?
Hover over row $n$ and compare its $n$ -th digit with the $n$ -th digit of $d$ .

Formal mathematicsF

The bijections and the diagonal, in Lean

A part as large as the whole. Mathlib's Equiv is a bijection packaged with its inverse. The doubling map pairs $\N$ with the even numbers.

doublingLean 4Formally verified

/-- The bijection `n ↦ 2n` between `ℕ` and the even numbers, with inverse `m ↦ m / 2`. -/
def doubling : ℕ ≃ {m : ℕ // Even m} where
  toFun n := ⟨2 * n, even_two_mul n⟩
  invFun m := m.1 / 2
  left_inv n := by simp
  right_inv m := by
    obtain ⟨m, k, hk⟩ := m
    apply Subtype.ext
    simp only
    omega

Axioms used: propext, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

The integers. The zigzag of Theorem 3, and the proof that it is a bijection. The tactic omega handles the arithmetic with n / 2 and n % 2.

zigzagLean 4Formally verified

/-- The zigzag enumeration of the integers: `0, −1, 1, −2, 2, −3, …`.
Even `n` goes to `n / 2`; odd `n` goes to `−(n + 1) / 2`. -/
def zigzag (n : ℕ) : ℤ :=
  if n % 2 = 0 then ((n / 2 : ℕ) : ℤ) else -((n / 2 : ℕ) : ℤ) - 1

Axioms used: No axiomsformal/Lumenary/Countability.leanTry it in the Lean web editor

zigzag_bijectiveLean 4Proved here from basic factsFormally verified

/-- **ℤ is countable**: the zigzag is a bijection `ℕ → ℤ`.
*Injective:* even inputs give values `≥ 0`, odd inputs give values `< 0`, and on each kind the
formula is one-to-one. *Surjective:* `z ≥ 0` is hit by `2z`, and `z < 0` by `−2z − 1`. -/
theorem zigzag_bijective : Bijective zigzag := by
  constructor
  · intro a b h
    unfold zigzag at h
    split_ifs at h <;> omega
  · intro z
    rcases le_or_gt 0 z with hz | hz
    · refine ⟨2 * z.toNat, ?_⟩
      unfold zigzag
      split_ifs <;> omega
    · refine ⟨(-2 * z - 1).toNat, ?_⟩
      unfold zigzag
      split_ifs <;> omega

Axioms used: propext, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

Pairs. To avoid division, the triangular number $T(d)$ is defined as the sum $0 + 1 + \dots + d$ . The proofs follow Theorem 4: values on one diagonal lie below the start of the next, and the walk steps from each value to the next.

triLean 4Formally verified

/-- The triangular number `tri d = 0 + 1 + ⋯ + d = d(d + 1)/2`: the number of points on the
diagonals `0, 1, …, d − 1` of the grid `ℕ × ℕ` (diagonal `j` has `j + 1` points). -/
def tri (d : ℕ) : ℕ := ∑ i ∈ range (d + 1), i

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

cantorPairLean 4Formally verified

/-- **Cantor's pairing function** `π(m, n) = tri (m + n) + n`: walk the grid diagonal by
diagonal; the point `(m, n)` lies on diagonal `m + n`, and is the `n`-th point along it. -/
def cantorPair (m n : ℕ) : ℕ := tri (m + n) + n

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

tri_succLean 4Applies a library theoremFormally verified

/-- Moving to the next diagonal adds `d + 1` points: `tri (d + 1) = tri d + (d + 1)`.
This is Mathlib's `Finset.sum_range_succ`. -/
theorem tri_succ (d : ℕ) : tri (d + 1) = tri d + (d + 1) := sum_range_succ _ _

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

tri_monoLean 4Proved here from basic factsFormally verified

/-- Triangular numbers increase: `tri a ≤ tri (a + k)`. -/
theorem tri_mono (a k : ℕ) : tri a ≤ tri (a + k) := by
  induction k with
  | zero => exact le_refl _
  | succ k ih => rw [← Nat.add_assoc, tri_succ]; omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

cantorPair_injectiveLean 4Proved here from basic factsFormally verified

/-- **Cantor's pairing is injective.** The values on diagonal `d` are `tri d, …, tri d + d`, all
less than `tri (d + 1)`, where the next diagonal starts. So equal values force equal diagonals
`m + n = m' + n'`, then equal positions `n = n'`, then `m = m'`. -/
theorem cantorPair_injective {m n m' n' : ℕ} (h : cantorPair m n = cantorPair m' n') :
    m = m' ∧ n = n' := by
  unfold cantorPair at h
  have key : ∀ {d d' n : ℕ}, d < d' → n ≤ d → tri d + n < tri d' := by
    intro d d' n hlt hn
    obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hlt
    have h1 := tri_mono (d + 1) k
    rw [Nat.add_right_comm] at h1
    have h2 := tri_succ d
    omega
  rcases lt_trichotomy (m + n) (m' + n') with hlt | heq | hgt
  · exact absurd h (Nat.ne_of_lt (lt_of_lt_of_le (key hlt (by omega)) (by omega)))
  · rw [heq] at h
    omega
  · exact absurd h (Nat.ne_of_gt (lt_of_lt_of_le (key hgt (by omega)) (by omega)))

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

cantorPair_surjectiveLean 4Proved here from basic factsFormally verified

/-- **Cantor's pairing is surjective**, by induction on the value `k`: if `π(m, n) = k`, the next
value `k + 1` is the next point of the walk — one step up the same diagonal, `(m − 1, n + 1)`, or,
at the end of a diagonal (`m = 0`), the first point `(n + 1, 0)` of the next one. -/
theorem cantorPair_surjective (k : ℕ) : ∃ m n, cantorPair m n = k := by
  induction k with
  | zero => exact ⟨0, 0, rfl⟩
  | succ k ih =>
    obtain ⟨m, n, h⟩ := ih
    unfold cantorPair at h
    cases m with
    | zero =>
      refine ⟨n + 1, 0, ?_⟩
      unfold cantorPair
      rw [Nat.add_zero, tri_succ]
      rw [Nat.zero_add] at h
      omega
    | succ m =>
      refine ⟨m, n + 1, ?_⟩
      unfold cantorPair
      rw [show m + (n + 1) = m + 1 + n by omega]
      omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

nat_prod_equivLean 4Proved here from basic factsFormally verified

/-- Hence **`ℕ × ℕ` has the same cardinality as `ℕ`**: Cantor's pairing is a bijection.
(Mathlib has a different pairing function with the same property, `Nat.pairEquiv`.) -/
theorem nat_prod_equiv : Nonempty (ℕ × ℕ ≃ ℕ) := by
  refine ⟨Equiv.ofBijective (fun p => cantorPair p.1 p.2) ⟨?_, ?_⟩⟩
  · intro p q h
    obtain ⟨h1, h2⟩ := cantorPair_injective h
    exact Prod.ext h1 h2
  · intro k
    obtain ⟨m, n, h⟩ := cantorPair_surjective k
    exact ⟨(m, n), h⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

Rationals and unions come from Mathlib:

rat_countableLean 4Applies a library theoremFormally verified

/-- **ℚ is countable**: Mathlib's instance, which encodes a fraction in lowest terms by its
numerator and denominator (`Rat.instDenumerable`). -/
theorem rat_countable : Countable ℚ := inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

countable_unionLean 4Applies a library theoremFormally verified

/-- **A countable union of countable sets is countable** (Mathlib's `Set.countable_iUnion`; its
proof uses the axiom of choice, which is part of Lean's logic, to pick an enumeration of each
set). -/
theorem countable_union {ι α : Type*} [Countable ι] (t : ι → Set α) (h : ∀ i, (t i).Countable) :
    (⋃ i, t i).Countable :=
  Set.countable_iUnion h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

cantorLean 4Proved here from basic factsFormally verified

/-- **Cantor's theorem**: no function `f : A → 𝒫(A)` is surjective. The *diagonal set*
`D = {a | a ∉ f a}` is missed: if `f a = D`, then `a ∈ D ↔ a ∉ f a ↔ a ∉ D`, which is impossible. -/
theorem cantor {α : Type*} (f : α → Set α) : ¬ Surjective f := by
  intro hf
  obtain ⟨a, ha⟩ := hf {x | x ∉ f x}
  have h : a ∈ f a ↔ a ∉ f a := by
    constructor
    · intro hin
      rw [ha] at hin
      exact hin
    · intro hout
      rw [ha]
      exact hout
  by_cases hin : a ∈ f a
  · exact h.mp hin hin
  · exact hin (h.mpr hin)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

cantor_libraryLean 4Applies a library theoremFormally verified

/-- Cantor's theorem from Mathlib: `Function.cantor_surjective`. -/
theorem cantor_library {α : Type*} (f : α → Set α) : ¬ Surjective f :=
  cantor_surjective f

Axioms used: No axiomsformal/Lumenary/Countability.leanTry it in the Lean web editor

The diagonal. An infinite 0–1 sequence is a function ℕ → Bool, and a list of them is s : ℕ → ℕ → Bool. The diagonal sequence differs from the n-th sequence at position n, so no list is complete.

diagonalLean 4Formally verified

/-- The **diagonal sequence** of a list `s₀, s₁, s₂, …` of infinite 0–1 sequences: its `n`-th
entry is the opposite of the `n`-th entry of `sₙ`. -/
def diagonal (s : ℕ → ℕ → Bool) : ℕ → Bool := fun n => !(s n n)

Axioms used: No axiomsformal/Lumenary/Countability.leanTry it in the Lean web editor

diagonal_neLean 4Proved here from basic factsFormally verified

/-- The diagonal sequence differs from the `n`-th sequence of the list — at position `n`. -/
theorem diagonal_ne (s : ℕ → ℕ → Bool) (n : ℕ) : diagonal s ≠ s n := by
  intro h
  have hn : diagonal s n = s n n := congrFun h n
  unfold diagonal at hn
  cases hs : s n n <;> simp [hs] at hn

Axioms used: propextformal/Lumenary/Countability.leanTry it in the Lean web editor

sequences_uncountableLean 4Proved here from basic factsFormally verified

/-- **The infinite 0–1 sequences cannot be listed**: no `s : ℕ → (ℕ → Bool)` is surjective,
because the diagonal sequence is never on the list. -/
theorem sequences_uncountable : ¬ ∃ s : ℕ → (ℕ → Bool), Surjective s := by
  rintro ⟨s, hs⟩
  obtain ⟨n, hn⟩ := hs (diagonal s)
  exact diagonal_ne s n hn.symm

Axioms used: propextformal/Lumenary/Countability.leanTry it in the Lean web editor

The decimal version: a digit sequence is a function ℕ → Fin 10. We prove the two properties the proof of Theorem 9 needs — the diagonal differs from the n-th expansion at digit n, and uses only the digits 4 and 5.

decimalDiagonalLean 4Formally verified

/-- The careful **decimal diagonal**: from a list of digit sequences `rₙ = 0.rₙ₀ rₙ₁ rₙ₂…`, take
digit `5` in position `n` unless `rₙ` has a `5` there, in which case take `4`. -/
def decimalDiagonal (r : ℕ → ℕ → Fin 10) : ℕ → Fin 10 := fun n => if r n n = 5 then 4 else 5

Axioms used: propextformal/Lumenary/Countability.leanTry it in the Lean web editor

decimalDiagonal_specLean 4Proved here from basic factsFormally verified

/-- The decimal diagonal (1) differs from the `n`-th expansion in the `n`-th digit, and (2) uses
only the digits `4` and `5` — never `0` or `9` — so it is the *only* decimal expansion of the
number it names (no `…4999…`/`…5000…` ambiguity). -/
theorem decimalDiagonal_spec (r : ℕ → ℕ → Fin 10) (n : ℕ) :
    decimalDiagonal r n ≠ r n n ∧ (decimalDiagonal r n = 4 ∨ decimalDiagonal r n = 5) := by
  unfold decimalDiagonal
  split_ifs with h
  · rw [h]
    exact ⟨by decide, Or.inl rfl⟩
  · exact ⟨fun h' => h h'.symm, Or.inr rfl⟩

Axioms used: propextformal/Lumenary/Countability.leanTry it in the Lean web editor

The real numbers and transcendental numbers. Mathlib proves that $\R$ is uncountable (via $|\R| = 2^{\aleph_0}$ ). Combining this with Mathlib's countability of the algebraic numbers gives Cantor's existence proof of transcendental numbers — which, like Cantor's, names no transcendental number.

real_uncountableLean 4Applies a library theoremFormally verified

/-- **ℝ is uncountable**: Mathlib's `Cardinal.not_countable_real`. -/
theorem real_uncountable : ¬ (Set.univ : Set ℝ).Countable :=
  Cardinal.not_countable_real

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

exists_transcendentalLean 4Proved here from basic factsFormally verified

/-- **Transcendental numbers exist** — Cantor's 1874 argument. The real numbers that are roots of
non-zero integer polynomials (the algebraic numbers) form a countable set (`Algebraic.countable`),
but `ℝ` is uncountable, so some real number is not algebraic. The proof names no such number. -/
theorem exists_transcendental : ∃ x : ℝ, Transcendental ℤ x := by
  by_contra h
  push Not at h
  apply real_uncountable
  apply (Algebraic.countable ℤ ℝ).mono
  intro x _
  have hx := h x
  unfold Transcendental at hx
  exact not_not.mp hx

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Countability.leanTry it in the Lean web editor

What is and is not formalised: the bijections of Theorems 2–4, Cantor's theorem, the diagonal argument for sequences, and the digit-level construction of Theorem 9 are proved here; the step "different expansions without 9-tails name different reals" is not, and the uncountability of $\R$ is taken from Mathlib.

ComputationC

Listing by machine

Listing the integers, pairs and rationalsPythonExact computationExhaustive finite checkComputationally tested

"""Listing the integers, the grid N x N and the positive rationals.

A set is countable when its elements can be listed a_0, a_1, a_2, ... with
every element appearing. This experiment runs three explicit listings:

* the zigzag 0, -1, 1, -2, 2, ... of the integers;
* Cantor's pairing function pi(m, n) = (m + n)(m + n + 1)/2 + n, which walks
  the grid N x N diagonal by diagonal, together with its inverse;
* the Calkin-Wilf sequence 1, 1/2, 2, 1/3, 3/2, 2/3, 3, ..., generated by
  Newman's rule x -> 1 / (2 floor(x) - x + 1), which lists every positive
  rational number exactly once.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from fractions import Fraction
from math import gcd, isqrt

def zigzag(n):
    """The n-th integer in the list 0, -1, 1, -2, 2, ..."""
    if n < 0:
        raise ValueError("n must be a natural number")
    return n // 2 if n % 2 == 0 else -(n // 2) - 1

def cantor_pair(m, n):
    """Cantor's pairing function: the position of (m, n) in the diagonal walk."""
    d = m + n
    return d * (d + 1) // 2 + n

def cantor_unpair(k):
    """Inverse of ``cantor_pair``: find the diagonal d with
    d(d + 1)/2 <= k < (d + 1)(d + 2)/2, then the position n along it."""
    if k < 0:
        raise ValueError("k must be a natural number")
    d = (isqrt(8 * k + 1) - 1) // 2
    n = k - d * (d + 1) // 2
    return d - n, n

def calkin_wilf(count):
    """The first ``count`` terms of the Calkin-Wilf sequence (Newman's rule)."""
    terms = []
    x = Fraction(1)
    for _ in range(count):
        terms.append(x)
        x = 1 / (2 * (x.numerator // x.denominator) - x + 1)
    return terms

def first_time_all_seen(terms, bound):
    """Number of terms needed before every reduced p/q with 1 <= p, q <= bound
    has appeared, or None if some never appears in ``terms``."""
    wanted = {Fraction(p, q) for p in range(1, bound + 1)
              for q in range(1, bound + 1) if gcd(p, q) == 1}
    for i, x in enumerate(terms):
        wanted.discard(x)
        if not wanted:
            return i + 1
    return None

def main():
    print("Zigzag listing of Z:", ", ".join(str(zigzag(n)) for n in range(11)),
          "...")
    print()
    print("Cantor's pairing pi(m, n), rows m = 0..4, columns n = 0..5:")
    for m in range(5):
        print("  m=%d: " % m + " ".join(f"{cantor_pair(m, n):3d}"
                                       for n in range(6)))
    limit = 100_000
    ok = all(cantor_pair(*cantor_unpair(k)) == k for k in range(limit))
    ok2 = all(cantor_unpair(cantor_pair(m, n)) == (m, n)
              for m in range(200) for n in range(200))
    print(f"pi(unpair(k)) = k for all k < {limit}: {ok}")
    print(f"unpair(pi(m, n)) = (m, n) for all m, n < 200: {ok2}")
    print()
    terms = calkin_wilf(2047)
    print("Calkin-Wilf:", ", ".join(str(x) for x in terms[:13]), "...")
    distinct = len(set(terms)) == len(terms)
    print(f"First {len(terms)} terms all different: {distinct}")
    n_all = first_time_all_seen(terms, 10)
    print(f"All 63 reduced p/q with p, q <= 10 appear within {n_all} terms.")
    print(f"Where is 3/5? Term number {terms.index(Fraction(3, 5)) + 1}.")
    print()
    print("Epistemic status: exact computation on finitely many values. It")
    print("illustrates the listings and checks them as far as it goes; that")
    print("they list every integer, pair and positive rational exactly once is")
    print("proved in the lesson (and for Calkin-Wilf in Calkin and Wilf, 2000).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Diagonal arguments on finite listsPythonExact computationExhaustive finite checkCounterexampleComputationally tested

"""Diagonal arguments, run on finite examples.

1. Cantor's theorem for a 3-element set A: there are 8^3 = 512 functions
   f : A -> P(A). For each one we form the diagonal set D = {a : a not in f(a)}
   and check that D is not a value of f, so no f is onto.
2. The decimal diagonal: for a list of ten numbers in [0, 1) we build a number
   whose n-th digit is 5, or 4 if the n-th number has a 5 there. It differs
   from the n-th number in the n-th digit, and its digits avoid 0 and 9.
3. Why avoid 0 and 9: the naive rule "replace digit x by 9 - x" applied to a
   cleverly chosen list produces 0.4999..., which is the same number as 0.5 -
   the first number on the list.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from decimal import Decimal, getcontext
from fractions import Fraction
from itertools import product

def subsets(elements):
    """All subsets of a finite collection, as frozensets."""
    elements = list(elements)
    return [frozenset(x for x, keep in zip(elements, mask) if keep)
            for mask in product([False, True], repeat=len(elements))]

def diagonal_set(f, domain):
    """Cantor's diagonal set {a in domain : a not in f(a)}."""
    return frozenset(a for a in domain if a not in f[a])

def check_cantor(n):
    """For A = {0, ..., n-1}, return (number of functions A -> P(A),
    number whose image misses the diagonal set, number that are onto)."""
    domain = list(range(n))
    power = subsets(domain)
    total = missed = onto = 0
    for values in product(power, repeat=n):
        f = dict(zip(domain, values))
        total += 1
        missed += diagonal_set(f, domain) not in values
        onto += set(values) == set(power)
    return total, missed, onto

def digits(x, k):
    """The first k digits after the point of x in [0, 1), from the expansion
    that does not end in repeating 9s. x is a Fraction or a Decimal."""
    out = []
    for _ in range(k):
        x *= 10
        d = int(x)                     # floor, as x >= 0
        out.append(d)
        x -= d
    return out

def diagonal_digits(rows):
    """Digit n is 5, or 4 when rows[n][n] == 5."""
    return [4 if row[n] == 5 else 5 for n, row in enumerate(rows)]

def numbers():
    """Ten labelled numbers in [0, 1)."""
    getcontext().prec = 50
    two, three, five = Decimal(2), Decimal(3), Decimal(5)
    return [("1/7", Fraction(1, 7)), ("1/2", Fraction(1, 2)),
            ("2/3", Fraction(2, 3)), ("5/11", Fraction(5, 11)),
            ("sqrt2 - 1", two.sqrt() - 1), ("sqrt3 - 1", three.sqrt() - 1),
            ("(sqrt5-1)/2", (five.sqrt() - 1) / 2), ("16/113", Fraction(16, 113)),
            ("1/81", Fraction(1, 81)), ("5/9", Fraction(5, 9))]

def main():
    total, missed, onto = check_cantor(3)
    print(f"1. A = {{0, 1, 2}}: {total} functions A -> P(A); the diagonal set is")
    print(f"   missing from the image of {missed} of them; {onto} are onto.")
    print()
    print("2. The decimal diagonal (diagonal digit in brackets):")
    named = numbers()
    rows = [digits(x, 10) for _, x in named]
    for n, ((label, _), row) in enumerate(zip(named, rows)):
        shown = "".join(f"[{d}]" if i == n else str(d) for i, d in enumerate(row))
        print(f"   {label:12} 0.{shown}...")
    diag = diagonal_digits(rows)
    print("   d          = 0." + "".join(map(str, diag)) + "...")
    ok = all(diag[n] != rows[n][n] for n in range(len(rows)))
    print(f"   d differs from number n in digit n, for every n: {ok}")
    print()
    tricky = [[5] + [0] * 9] + [[0] * 10 for _ in range(9)]
    naive = [9 - row[n] for n, row in enumerate(tricky)]
    print("3. List 0.5000..., 0.0000..., 0.0000..., ... with the naive rule")
    print("   'replace x by 9 - x' gives 0." + "".join(map(str, naive))
          + "... = 0.5, which IS on the list.")
    print()
    print("Epistemic status: exhaustive for the 512 functions of part 1 and")
    print("exact for parts 2 and 3, but finite. The theorems - for every set")
    print("and every infinite list - are the lesson's proofs. Part 3 is a")
    print("counterexample to a careless version of the argument, not to Cantor.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Both experiments are finite. The first checks the listings on the first hundred thousand values; that they work for every value is what Theorems 3 and 4 prove. The second runs the diagonal construction on lists of ten numbers — and part 3 shows why the proof of Theorem 9 must avoid the digits 0 and 9.

Exercises

1. Countability and Cantor's diagonal argument

Warm-upHuman

The zigzag $z : \N \to \Z$ lists the integers as $z(0), z(1), z(2), \dots = 0, -1, 1, -2, 2, \dots$ What is $z(7)$ ?

2. Countability and Cantor's diagonal argument

Warm-upHuman

Compute Cantor's pairing $\pi(2, 3) = \dfrac{(m + n)(m + n + 1)}{2} + n$ for $m = 2$ , $n = 3$ .

3. Countability and Cantor's diagonal argument

CoreHuman

Which pair $(m, n)$ has $\pi(m, n) = 12$ ?

Choose one

(2, 2)

(3, 1)

(1, 3)

(0, 4)

4. Countability and Cantor's diagonal argument

CoreHuman

Which of these sets are countable? (Choose all that apply.)

Choose all that apply

5. Countability and Cantor's diagonal argument

CoreHuman

A list begins $r_1 = 0.5123\ldots$ , $r_2 = 0.3456\ldots$ , $r_3 = 0.9995\ldots$ . Using the lesson's rule (digit $n$ of $x$ is $4$ if digit $n$ of $r_n$ is $5$ , and $5$ otherwise), how does $x$ begin?

Choose one

0.455\ldots

0.544\ldots

0.555\ldots

0.459\ldots

6. Countability and Cantor's diagonal argument

CoreHuman

After seeing the diagonal argument, Kofi says: “Fine, the list missed $x$ . So put $x$ at the front of the list — now nothing is missing.” What is the best reply?

Choose one

The new list has its own diagonal number, which is missing from it. The argument shows that every list misses a number.You are not allowed to change the list.The list is infinite, so there is no front to put it at.Kofi is right; the argument only shows that some lists are incomplete.

7. Countability and Cantor's diagonal argument

CoreHuman

Let $A = \{1, 2, 3\}$ and define $f : A \to \mathcal{P}(A)$ by $f(1) = \{1, 2\}$ , $f(2) = \{3\}$ , $f(3) = \{1, 3\}$ . List the elements of Cantor's diagonal set $D = \{a \in A : a \notin f(a)\}$ .

8. Countability and Cantor's diagonal argument

Warm-upHuman

How many elements does $\mathcal{P}(\mathcal{P}(\{1, 2\}))$ have?

9. Countability and Cantor's diagonal argument

CoreFormal

Which Lean statement expresses Cantor's theorem for a type α?

Choose one

∀ f : α → Set α, ¬ Function.Surjective f∀ f : α → Set α, ¬ Function.Injective f∀ f : Set α → α, ¬ Function.Surjective f∃ f : α → Set α, Function.Bijective f

10. Countability and Cantor's diagonal argument

StretchComputational

Write pair(m, n) computing Cantor's $\pi(m, n) = (m+n)(m+n+1)/2 + n$ , and its inverse unpair(k), which returns the pair (m, n) with pair(m, n) == k. (Hint: find the diagonal $d = m + n$ as the largest $d$ with $d(d+1)/2 \le k$ .)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"A proper subset of an infinite set must be smaller." The even numbers are a proper subset of $\N$ , yet $n \mapsto 2n$ matches them perfectly with $\N$ . For infinite sets "part" does not imply "smaller" — Dedekind even used this property to define infinite sets.

Misconception

"Just add the diagonal number to the list." You can — but the new list has a new diagonal, which is missing from it. The theorem is not that one particular list is incomplete; it is that every list is.

Misconception

Forgetting that $0.4999\ldots = 0.5$ . A careless diagonal rule might produce $0.4999\ldots$ , which equals $0.5$ and may well be on the list. The proof avoids the problem by never using the digits 0 and 9.

Misconception

" $\Q$ is dense — between any two rationals there is another — so it must be uncountable." Density is about order, countability about matching. $\Q$ is dense and countable; Theorem 5 lists it.

Misconception

"Countable means we could finish counting." A countably infinite set can never be counted to the end. Countable means each element appears at some finite position in one infinite list.

ViewpointsH

Many ways of seeing

Analysis— countable sets have length zero

Cover the $n$ -th point of a countable set $\{q_0, q_1, q_2, \dots\} \subseteq \R$ by an interval of length $\varepsilon / 2^{n+1}$ . The intervals have total length at most $\varepsilon/2 + \varepsilon/4 + \dots = \varepsilon$ , for any $\varepsilon > 0$ we like. So every countable set — $\Q$ included — has measure zero. Since $[0, 1]$ has length $1$ (and one can prove it cannot be covered by countably many intervals of total length less than $1$ ), this gives a second proof that $[0, 1]$ is uncountable, and says more: the rationals, although dense, are a negligible part of the line.

Topology— the Baire category theorem

A third proof comes from topology. The Baire category theorem says that a non-empty complete metric space, such as $\R$ , is not a countable union of nowhere dense sets (closed sets containing no interval). A single point is nowhere dense, so $\R$ is not a countable union of points: it is uncountable. The same theorem shows that a non-empty complete metric space with no isolated points — the Cantor set, for instance — is uncountable, and it is a workhorse of analysis, for example in showing that "most" continuous functions are nowhere differentiable.

Number theory— algebraic and transcendental

Counting separates the algebraic numbers (countable) from the transcendental ones (uncountable, so "almost all" real numbers). Yet proving that a particular number is transcendental is hard: Liouville (1844), Hermite for $e$ (1873), Lindemann for $\pi$ (1882), and the Gelfond–Schneider theorem (1934) for numbers such as $2^{\sqrt{2}}$ . Whether $e + \pi$ is irrational is still unknown. Cantor's argument shows the transcendental numbers are everywhere; number theory is the art of catching one.

Computation— most numbers cannot be computed

A computer program is a finite string of symbols from a finite alphabet, so there are only countably many programs. A real number is computable if some program prints its decimal digits one after another for ever. Hence only countably many real numbers are computable, and almost all real numbers can never be computed by any program. Alan Turing (1936) used a diagonal argument in the same spirit to show that no program can decide, for every program, whether it eventually halts; see computability.

Logic— diagonal arguments elsewhere

The diagonal pattern reappears across logic: in Russell's paradox (next door, in Russell's paradox), in Turing's halting problem, and — in spirit, though the construction is different — in Gödel's incompleteness theorems, whose key step is a sentence that says of itself that it is unprovable; see incompleteness.

Wonder Trails

Wonder Trail

Wonder Trail · Optional · never gradedHow many infinities?There are infinitely many counting numbers and infinitely many infinite 0–1 sequences. Are these two infinities the same size?Follow the trail

History & global context

History and global context

Ancient and medieval puzzles. Greek philosophers debated the infinite since Zeno; Aristotle accepted only "potential" infinity. Jaina cosmological texts in India, from roughly the last centuries BCE, classified quantities as enumerable, innumerable and infinite, and distinguished several kinds of infinity — a striking early recognition, in a very different framework from Cantor's, that "infinite" need not be one thing.
Galileo (Two New Sciences, 1638) matched the squares with the counting numbers and concluded that infinite quantities cannot be compared. Bernard Bolzano's Paradoxes of the Infinite (published 1851) took matchings of infinite sets seriously.
Georg Cantor proved in 1874 that the algebraic numbers are countable and the real numbers are not (his first proof used nested intervals, not diagonals). In 1877 he found a bijection between a line segment and a square and wrote to Richard Dedekind, "Je le vois, mais je ne le crois pas" — "I see it, but I don't believe it". The diagonal argument appeared in 1891. Cantor's ideas met fierce opposition from some contemporaries, but David Hilbert declared in 1925 that "no one shall expel us from the paradise that Cantor has created".
Independence. Kurt Gödel (1940) and Paul Cohen (1963) settled the logical status of Cantor's continuum hypothesis: it is independent of the usual axioms. Cohen received the Fields Medal in 1966 for this work.

The hotel with infinitely many rooms

Counting is matching

Definitions

Sets that can be listed

Sets that cannot be listed

Explore: the diagonal machine

The bijections and the diagonal, in Lean

Listing by machine

Exercises

Common misconceptions

Many ways of seeing

Wonder Trail

History and global context

Further reading