Counting & logic

Cantor’s diagonal argument

An infinite theorem with a short proof: build a predicate that cannot appear in any proposed complete list.

-- Top 100 #63: Cantor’s diagonal argument
-- History: 1891 · Cantor.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The diagonal predicate disagrees with each proposed row at that row’s own index.
-- Scope: Proves that no map from any type α onto its predicates α → Prop can be surjective. This is the predicate form of Cantor’s theorem.
-- Source: https://lurch.plus/100/

theorem cantor {α : Type} (f : α → α → Prop) :
    ¬ (∀ s : α → Prop, ∃ a, f a = s) := by
  intro onto
  -- Ask for the row representing “not on your own diagonal”.
  obtain ⟨a, ha⟩ := onto (fun x => ¬ f x x)
  have h := congrArg (fun s => s a) ha
  -- h says f a a is equivalent to its own negation.
  have hn : ¬ f a a := fun hp => (h.mp hp) hp
  exact hn (h.mpr hn)

Explanation

`α → Prop`

A predicate on α represents a subset: it states which elements belong.

`congrArg`

Apply the same function to both sides of an equality.

`¬ P`

Negation is a function from a proof of P to False.

Background and proof scope

1891 · Cantor

The diagonal predicate disagrees with each proposed row at that row’s own index.

Proves that no map from any type α onto its predicates α → Prop can be surjective. This is the predicate form of Cantor’s theorem.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Read the final two lines as a paper proof. Where exactly is the contradiction?