Cantorの対角線論法

今回はLean4でCantorの定理（と同等の定理）を証明します。

※厳密なCantorの定理はCardinalを定義する必要がありますので、その話はまた別の機会に行いたいと思います。

Lean4でCantorの定理は以下でかけます。

def Set (α : Type u) := α → Prop
instance : Membership α (Set α) := ⟨fun a s => s a⟩
def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
----- ( ここまで道具の準備 ) -----

theorem cantor_surjective {α: Type u}
  (f : α → Set α) : ¬ surjective f := by {
  -- write your proof here
  sorry;
}

これをLean4で解いてみます。

Cantorの定理を証明する場合、αのある部分集合を使って証明する手法がよく採用されます。

この補題を絡めて、証明を途中まで埋めます。

theorem cantor_surjective {α: Type u}
  (f : α → Set α) : ¬ surjective f := by {
  /- Hint: Use the set { a | a ∉ f a} in Set α. -/

  -- fが全射であると仮定して矛盾を導く.
  intro h;

  -- 任意のa∈αに対し f(a)≠a in αとなる部分集合をaug_setと置く.
  let aug_set : Set α := (fun a => (a ∉ f a));

  -- fが全射であるという仮定より f(D)=B なる D∈α が存在する.
  let ⟨D, e⟩ := h aug_set;

  sorry;
}

// この時点のtactic state
  α : Type u
  f : α → Set α
  h : surjective f
  aug_set : Set α := fun a => ¬a ∈ f a
  D : α
  e : f D = aug_set
  ⊢ False

Cantorの補題の証明は [katex]a \in A[/katex] と、[katex]a \notin A[/katex] についてどちらも矛盾となることで示します。

Lean4の証明でもその方針で証明してみます。Lean4で排中律を使いたい場合は by_cases を使います。

  ...(省略)...

  -- (D ∈ f D) と (D ∉ f D)の両方の場合について考える.
  by_cases h : (D ∈ f D);

  -- case D ∈ f D
  case inl => {sorry;}

  -- case D ∉ f D
  case inr => {sorry;}

// この時点のtactic state
 case inl
  α : Type u
  f : α → Set α
   : surjective f
  aug_set : Set α := fun a => ¬a ∈ f a
  D : α
  e : f D = aug_set
  h : D ∈ f D
  ⊢ False
  
  case inr
  α : Type u
  f : α → Set α
   : surjective f
  aug_set : Set α := fun a => ¬a ∈ f a
  D : α
  e : f D = aug_set
  h : ¬D ∈ f D
  ⊢ False

sorryの部分を埋めます。

D ∈ f D の場合

  -- case D ∈ f D
  case inl => {
    have : D ∉ f D := by {
      -- by construnction
      simp [e] at h;
      exact h;
    };
    contradiction;
  }

D ∉ f D の場合

  -- case D ∉ f D
  case inr => {
    have : D ∈ f D := by {
      -- by construnction
      have : aug_set D := h;
      rw [←e] at this;
      exact this;
    };
    contradiction;
  }

// この時点のtactic state
  Goals accomplished 🎉

準備を含んだ完全な証明は以下となります。

def Set (α : Type u) := α → Prop
instance : Membership α (Set α) := ⟨fun a s => s a⟩
def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
----- ( ここまで道具の準備 ) -----

theorem cantor_surjective {α: Type u}
  (f : α → Set α) : ¬ surjective f := by {
  intro h;
  let aug_set : Set α := (fun a => (a ∉ f a));
  let ⟨D, e⟩ := h aug_set;
  by_cases h : (D ∈ f D);
  -- case D ∈ f D
  case inl => {
    have : D ∉ f D := by {
      simp [e] at h;
      exact h;
    };
    contradiction;
  }
  -- case D ∉ f D
  case inr => {
    have : D ∈ f D := by {
      have : aug_set D := h;
      rw [←e] at this;
      exact this;
    };
    contradiction;
  }
}

参考：

mathlib documentation (web)