Cantor の定理

Cantor の定理とは、次のような定理です。

「濃度」とは、集合の「要素の個数」という概念を無限集合にも拡張したものであり、おおむね「一対一で漏れのない対応がつけられるならば、要素数が等しいと言ってよいだろう」というアイデアに基づくものです。

この Cantor の定理はよく知られたものであり、Mathlib には既に存在しますが、ここでは Lean を用いて数学理論を形式化するとはどういうことかお見せするために、Mathlib を一切使わずに形式化していきます。

集合論の形式化

全体集合を固定する

まず、集合の概念を Lean で表現する必要があります。

Lean の型 T : Type は直観的には「項の集まり」を意味するので、これをそのまま集合だと考えてしまって、t : T をもって t ∈ T であると見なせばよいように思えるかもしれません。しかし Lean の型システムの性質上、この解釈は途中で破綻します。

たとえば S T : Type に対して共通部分の S ∩ T の要素は S にも T にも属していなくてはいけませんが、これは型の一意性から実現できません。S ∪ T についても同様で、S にも S ∪ T にも属している要素に正しく型をつけることができません。

そこで全体集合 α : Type を固定して、その中に含まれる集まりだけを考えることにします。

/-- α を全体集合として、その部分集合の全体。
α の部分集合と α 上の述語を同一視していることに注意。 -/
def Set (α : Type) := α → Prop

variable {α : Type}

/-- `a : α` は集合 `s` に属する。数学では普通 `a ∈ s` と書かれる。 -/
def Set.mem (s : Set α) (a : α) : Prop := s a

/-- `s a` を `a ∈ s` と書けるようにする。 -/
instance : Membership α (Set α) := ⟨Set.mem⟩

/-- `A B : Set α` に対する共通部分 -/
def Set.inter (A B : Set α) : Set α := fun x => x ∈ A ∧ x ∈ B

/-- `A B : Set α` に対する合併 -/
def Set.union (A B : Set α) : Set α := fun x => x ∈ A ∨ x ∈ B

このようにしておくと、上記の問題は回避することができ、S T : Set α の共通部分や合併をとることができます。

内包記法の定義

「述語と部分集合を同一視する」という表現の良くないところは、集合を関数として扱うことになるので表記がわかりにくくなり、混乱を招きかねないということです。述語 p : α → Prop に対して内包記法 {x : α | p x} が使用できるようにしましょう。

Lean のメタプログラミングフレームワークの力を借りれば、そうしたことも可能です。

variable {α : Type}

/-- 述語 `p : α → Prop` に対応する集合 -/
def setOf {α : Type} (p : α → Prop) : Set α := p

/-- 内包表記 `{ x : α | p x }` の `x : α` の部分のための構文。
`: α` の部分はあってもなくてもよいので `( )?` で囲っている。-/
syntax extBinder := ident (" : " term)?

/-- 内包表記 `{ x : α | p x }` の `{ | }` の部分のための構文。 -/
syntax (name := setBuilder) "{" extBinder " | " term "}" : term

/-- 内包表記の意味をマクロとして定義する -/
macro_rules
  | `({ $x:ident : $type | $p }) => `(setOf (fun ($x : $type) => $p))
  | `({ $x:ident | $p }) => `(setOf (fun ($x : _) => $p))

-- 内包表記が使えるようになったが、コマンドの出力や infoview では
-- いま定義した記法が使われないという問題がある
/-- info: setOf fun n => ∃ m, n = 2 * m : Set Nat -/
#guard_msgs in
  #check {n : Nat | ∃ m, n = 2 * m}

/-- infoview やコマンドの出力でも内包表記を使用するようにする -/
@[app_unexpander setOf]
def setOf.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $x:ident => $p) => `({ $x:ident | $p })
  | `($_ fun ($x:ident : $ty:term) => $p) => `({ $x:ident : $ty:term | $p })
  | _ => throw ()

-- 正常に動作することを確認

/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/
#guard_msgs in
  #check {n | ∃ m, n = 2 * m}

/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/
#guard_msgs in
  #check {n : Nat | ∃ m, n = 2 * m}

全射と単射

関数 f : A → B が全射であるとは、任意の b : B に対して f a = b となる a : A が存在することです。また、f が単射であるとは、任意の a₁, a₂ : A に対して f a₁ = f a₂ ならば a₁ = a₂ となることです。

これを Lean で表現すると次のようになります。

variable {α β : Type}

/-- 関数の全射性 -/
def Function.Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b

/-- 関数の単射性 -/
def Function.Injective (f : α → β) : Prop := ∀ {a₁ a₂ : α}, f a₁ = f a₂ → a₁ = a₂

問1: 全射バージョン

以上の準備のもとで、Cantor の定理を証明することができます。まずは全射バージョンから示しましょう。次の sorry の部分を埋めてください。

variable {α : Type}

open Function

/-- ある集合からそのベキ集合への全射は存在しない -/
theorem cantor_surjective (f : α → Set α) : ¬ Surjective f := by
  -- `f` が全射であると仮定する
  intro hsurj

  -- 反例になる集合 `A` を構成する
  let A : Set α := sorry

  -- `f` は全射なので、ある `a` が存在して `f a = A`
  obtain ⟨a, ha⟩ := hsurj A

  -- `a ∈ A` は `a ∉ A` と同値である
  have : a ∈ A ↔ a ∉ A := by
    sorry

  -- これは矛盾
  simp at this

問2: 単射バージョン

単射バージョンも示すことができます。次の sorry の部分を埋めてください。

/-- ベキ集合から元の集合への単射は存在しない -/
theorem cantor_injective (f : Set α → α) : ¬ Injective f := by
  -- `f` が単射だと仮定する
  intro hinj

  -- 反例になる集合 `A` を構成する
  let A : Set α := sorry

  -- このとき `f A ∈ A` と `f A ∉ A` が同値になる
  have : (f A ∈ A) ↔ (f A ∉ A) := by
    sorry

  -- これは矛盾である
  simp at this