正本：FormalLab/Mathematics/Cardinality.lean

第25章：有限性・可算性・基数・無限#

自然数と偶数にはどちらも無限に多くの要素があります。偶数は自然数の一部分ですが、写像 n ↦ 2n によって自然数全体と一対一に対応します。一方、自然数から真偽値列全体への列挙をどのように選んでも、その一覧に現れない列を対角線上の値を反転して構成できます。

本章では要素数を数値へ還元せず、単射・全射・全単射の存在によって型の大きさを比較します。有限、可算以下、可算無限を区別し、Cantorの対角線論法をBool値関数についてLeanで証明します。最後に、基数としての大きさとLeanの宇宙レベルが異なる分類であることを明確にします。

大きさを写像で比較する#

型 A から B への単射があれば、A の異なる要素を潰さず B の中へ配置できます。このとき |A| ≤ |B| と読みます。全単射があれば |A| = |B| と読みますが、これはA = Bという型の等式ではありません。大きさが同じでも、要素の意味や演算は異なり得ます。

\begin{aligned} |A|\le |B|&\;:\!\Longleftrightarrow\;\exists f:A\to B.\;\mathsf{Injective}(f),\\ |A|=|B|&\;:\!\Longleftrightarrow\;\exists f:A\to B.\;\mathsf{Bijective}(f). \end{aligned}

有限性は、ある自然数 n に対してAが0, …, n-1と全単射になることです。本章では標準の Fin nを再実装せず、必要な比較を関数の性質として直接表します。

Leankernel-checked counterpartL33–43

namespace FormalLab.Mathematics.Cardinality

universe u v

open FormalLab.Mathematics.FunctionProperties

def CardinalLE (A : Type u) (B : Type v) : Prop :=
  ∃ f : A → B, IsInjective f

def Equinumerous (A : Type u) (B : Type v) : Prop :=
  ∃ f : A → B, IsBijective f

ある有限順序型 Fin n と全単射である、という有限性です。

Leankernel-checked counterpartL46–71

def IsFinite (A : Type u) : Prop :=
  ∃ n : Nat, Equinumerous A (Fin n)

def AtMostCountable (A : Type u) : Prop :=
  CardinalLE A Nat

def CountablyInfinite (A : Type u) : Prop :=
  Equinumerous A Nat

def boolToFin : Bool → Fin 2
  | false => 0
  | true => 1

theorem boolToFinBijective : IsBijective boolToFin where
  injective := by
    intro a b equal
    cases a <;> cases b <;> simp [boolToFin] at equal ⊢
  surjective := by
    rintro ⟨value, bound⟩
    have alternatives : value = 0 ∨ value = 1 := by omega
    rcases alternatives with rfl | rfl
    · exact ⟨false, rfl⟩
    · exact ⟨true, rfl⟩

theorem boolIsFinite : IsFinite Bool :=
  ⟨2, boolToFin, boolToFinBijective⟩

偶数は自然数と同じ基数を持つ#

Leankernel-checked counterpartL75–103

def EvenNat := {n : Nat // n % 2 = 0}

def toEven (n : Nat) : EvenNat :=
  ⟨2 * n, by simp⟩

def fromEven (n : EvenNat) : Nat :=
  n.val / 2

theorem toEvenInjective : IsInjective toEven := by
  intro a b equal
  have values : 2 * a = 2 * b := congrArg Subtype.val equal
  exact Nat.mul_left_cancel (by decide) values

theorem fromEvenToEven (n : Nat) : fromEven (toEven n) = n := by
  simp [fromEven, toEven]

theorem toEvenFromEven (n : EvenNat) : toEven (fromEven n) = n := by
  apply Subtype.ext
  exact Nat.mul_div_cancel' (Nat.dvd_of_mod_eq_zero n.property)

theorem evenCountablyInfinite : CountablyInfinite EvenNat := by
  refine ⟨fromEven, ⟨leftInverseGivesInjective toEvenFromEven, ?_⟩⟩
  intro n
  exact ⟨toEven n, fromEvenToEven n⟩

theorem evenAtMostCountable : AtMostCountable EvenNat := by
  refine ⟨Subtype.val, ?_⟩
  intro a b equal
  exact Subtype.ext equal

fromEvenToEven と toEvenFromEven は、二つの関数が互いに逆であることを各向きに証明します。したがって evenCountablyInfinite は自然数と偶数の全単射を実際に構成しています。両方向の単射から全単射を得るCantor–Schröder–Bernstein定理は一般には別の証明を要し、任意の二単射が互いの逆になるわけではありません。

有限集合が真部分集合と同じ大きさを持たないのに対し、自然数は偶数という真部分集合と同じ大きさを持ちます。この性質は無限性の一つの特徴づけですが、基礎理論によってDedekind無限と他の無限概念の関係には選択原理が関与します。ここでは「無限」を無条件に一つの定義へ固定しません。

対角線上で列挙から逃れる#

α → Bool は、αで添字づけられた真偽値列です。関数table : α → (α → Bool)を、各aに一行の真偽値列を割り当てる表とみなします。対角列diagonal a = !(table a a)は、行aと位置aで必ず異なります。したがってどの行とも等しくありません。

Leankernel-checked counterpartL122–135

def diagonal {α : Type u} (table : α → α → Bool) : α → Bool :=
  fun a => !(table a a)

theorem diagonalDiffers {α : Type u} (table : α → α → Bool) (a : α) :
    diagonal table ≠ table a := by
  intro equal
  have point := congrFun equal a
  simp [diagonal] at point

theorem noSurjectionToBoolPowers {α : Type u} :
    ¬ ∃ table : α → (α → Bool), IsSurjective table := by
  rintro ⟨table, surjective⟩
  obtain ⟨a, equal⟩ := surjective (diagonal table)
  exact diagonalDiffers table a equal.symm

この証明は「無限だから大きい」という印象に依存しません。型αが有限でも無限でも、 α → Boolをαで全射的に列挙することはできません。各候補行へ一か所で異なる列を同じ表から構成するためです。Bool値関数は部分集合の特性関数に相当しますが、一般のProp値述語と Boolを同一視せず、ここでは計算可能な反転を使うためBoolを選んでいます。

可算以下と可算無限を区別する#

AtMostCountable AはAから自然数への単射を要求します。空型や有限型も可算以下です。 CountablyInfinite Aは自然数との全単射を要求するため、有限型を除外します。「可算」という語は文献によって有限を含む場合と可算無限だけを指す場合があるので、本書では二語を使い分けます。

Leankernel-checked counterpartL150–158

theorem emptyAtMostCountable : AtMostCountable Empty := by
  refine ⟨(fun impossible : Empty => nomatch impossible), ?_⟩
  intro a _b _equal
  nomatch a

theorem boolAtMostCountable : AtMostCountable Bool := by
  refine ⟨fun b => if b then 1 else 0, ?_⟩
  intro a b equal
  cases a <;> cases b <;> simp at equal ⊢

基数と宇宙レベルは異なる#

Type uの宇宙レベルは、型式をどのsortへ分類するかを管理します。基数はある型の要素が別の型へ単射・全単射で対応するかを測ります。同じ宇宙に異なる基数の型が多数あり、宇宙レベルが高い型でも要素を一つしか持たない場合があります。したがってType 1を「Type 0より要素数が大きい型」とは読みません。

宇宙は全ての小さい型を型検査上どこへ置くかという問題に答え、基数は固定した二型の要素対応に答えます。Cantorの定理から冪型が元の型より真に大きいことを論じる際にも、その命題を述べる宇宙と、比較対象の基数を別々に追跡します。

要点#

型の大きさは単射で比較し、全単射で同じ基数であることを表す。
可算以下は有限型を含み、可算無限は自然数との全単射を要求する。
無限型は真部分型と全単射になり得るが、無限概念間の同値には基礎理論上の仮定が関与する。
対角線論法は任意の列挙候補から、その一覧にない対象を構成する。
基数は要素対応、Leanの宇宙レベルは型式の分類であり、同じ尺度ではない。

研究史と文献案内#

Cantorの1874年論文 [CAN74] は代数的数の可算性と実数の非可算性を扱います。本章の一般化された真偽値列の対角線証明や、後世の基数算術を同論文の記法へそのまま帰属させません。Dedekindの無限系 [DED88]、Zermeloの集合論公理化 [ZER08] とも基礎づけの役割を分けて読みます。

問題#

単射・全射・全単射で三種類の比較を作る#

Bool、Nat、EvenNatの各組について単射または全射を具体的に構成し、全単射まで得られる組を判定してください。関数の始域・終域を省略せず、同じ式でも終域を変えると全射性が変わる例を含めます。「部分集合だから小さい」という推論が無限の場合に不十分な理由をtoEvenから説明します。

対角線証明を表として追跡する#

三行三列の有限な真偽値表を一つ作り、対角成分を反転した列を書いてください。その列が各行と異なる位置を一つずつ示します。次にdiagonalDiffersのcongrFunがこの一点比較へ対応することを説明し、有限表では新しい列が表の列数を越えるだけで、一般定理の論理が有限性に依存しないことを確認します。

可算性と宇宙を別々の判断へ戻す#

Nat : Type、Type : Type 1、AtMostCountable Natを三つの異なる主張として展開してください。宇宙レベルを一段持ち上げたULift NatとNatの間に全単射を構成し、宇宙が変わっても要素対応が保存される例を示します。[CAN74]の実数非可算性と本章のBool冪型定理の論証形式も比較します。