(* Title: HOL/Isar_Examples/Cantor.thy Author: Makarius *) section ‹Cantor's Theorem› theory Cantor imports Main begin subsection ‹Mathematical statement and proof› text ‹ Cantor's Theorem states that there is no surjection from a set to its powerset. The proof works by diagonalization. E.g.\ see ▪ 🌐‹http://mathworld.wolfram.com/CantorDiagonalMethod.html› ▪ 🌐‹https://en.wikipedia.org/wiki/Cantor's_diagonal_argument› › theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x" proof assume "∃f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x" then obtain f :: "'a ⇒ 'a set" where *: "∀A. ∃x. A = f x" .. let ?D = "{x. x ∉ f x}" from * obtain a where "?D = f a" by blast moreover have "a ∈ ?D ⟷ a ∉ f a" by blast ultimately show False by blast qed subsection ‹Automated proofs› text ‹ These automated proofs are much shorter, but lack information why and how it works. › theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A" by best theorem "∄f :: 'a ⇒ 'a set. ∀A. ∃x. f x = A" by force subsection ‹Elementary version in higher-order predicate logic› text ‹ The subsequent formulation bypasses set notation of HOL; it uses elementary ‹λ›-calculus and predicate logic, with standard introduction and elimination rules. This also shows that the proof does not require classical reasoning. › lemma iff_contradiction: assumes *: "¬ A ⟷ A" shows False proof (rule notE) show "¬ A" proof assume A with * have "¬ A" .. from this and ‹A› show False .. qed with * show A .. qed theorem Cantor': "∄f :: 'a ⇒ 'a ⇒ bool. ∀A. ∃x. A = f x" proof assume "∃f :: 'a ⇒ 'a ⇒ bool. ∀A. ∃x. A = f x" then obtain f :: "'a ⇒ 'a ⇒ bool" where *: "∀A. ∃x. A = f x" .. let ?D = "λx. ¬ f x x" from * have "∃x. ?D = f x" .. then obtain a where "?D = f a" .. then have "?D a ⟷ f a a" by (rule arg_cong) then have "¬ f a a ⟷ f a a" . then show False by (rule iff_contradiction) qed subsection ‹Classic Isabelle/HOL example› text ‹ The following treatment of Cantor's Theorem follows the classic example from the early 1990s, e.g.\ see the file @{verbatim "92/HOL/ex/set.ML"} in Isabelle92 or @{cite ‹\S18.7› "paulson-isa-book"}. The old tactic scripts synthesize key information of the proof by refinement of schematic goal states. In contrast, the Isar proof needs to say explicitly what is proven. ━ Cantor's Theorem states that every set has more subsets than it has elements. It has become a favourite basic example in pure higher-order logic since it is so easily expressed: @{text [display] ‹∀f::α ⇒ α ⇒ bool. ∃S::α ⇒ bool. ∀x::α. f x ≠ S›} Viewing types as sets, ‹α ⇒ bool› represents the powerset of ‹α›. This version of the theorem states that for every function from ‹α› to its powerset, some subset is outside its range. The Isabelle/Isar proofs below uses HOL's set theory, with the type ‹α set› and the operator ‹range :: (α ⇒ β) ⇒ β set›. › theorem "∃S. S ∉ range (f :: 'a ⇒ 'a set)" proof let ?S = "{x. x ∉ f x}" show "?S ∉ range f" proof assume "?S ∈ range f" then obtain y where "?S = f y" .. then show False proof (rule equalityCE) assume "y ∈ f y" assume "y ∈ ?S" then have "y ∉ f y" .. with ‹y ∈ f y› show ?thesis by contradiction next assume "y ∉ ?S" assume "y ∉ f y" then have "y ∈ ?S" .. with ‹y ∉ ?S› show ?thesis by contradiction qed qed qed text ‹ How much creativity is required? As it happens, Isabelle can prove this theorem automatically using best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space. The context of Isabelle's classical prover contains rules for the relevant constructs of HOL's set theory. › theorem "∃S. S ∉ range (f :: 'a ⇒ 'a set)" by best end