$ \newcommand{\exi}{\exists\,} \newcommand{\all}{\forall} \newcommand{\equ}{\!=\!} \newcommand{\nequ}{\!\neq\!} \newcommand{\amp}{\;\&\;} \renewcommand{\Set}[2]{\left\{\;#1\mathrel{}\middle|\mathrel{}#2\;\right\}} \newcommand{\parenth}[1]{\left(\;#1\;\right)} \newcommand{\braces}[1]{\left\{\;#1\;\right\}} \newcommand{\bracket}[1]{\left[\;#1\;\right]} \newcommand{\godel}[1]{\left\ulcorner #1 \right\urcorner} $

論理式の一意性記号について

論理式の一意性記号について以下のように定義する:

\begin{align} \exists!xA(x) \equiv \exists x \left[ A(x) \land \forall y \left( A(y) \Rightarrow x = y \right) \right] \end{align}
この時、$(x,y)$が組として一意に存在する意味で$\exists!x \exists!y A(x,y)$を書くのは間違っている。 なぜなら前者は論理式で表記すると、 $$ \exists x, y \left[ A(x,y) \land \forall z, w \left( A(z,w) \Rightarrow x = z \land y = w \right) \right] $$ であって、後者は、$\exists!$の定義にしたがって展開すると、 \begin{array}{rcl} \exists!x \exists!y A(x,y) & \equiv & \exists x \left[ \exists! y A(x,y) \land \forall x\prime \left( \exists! y A(x\prime,y) \Rightarrow x = x\prime \right) \right] \\ & \equiv & \exists x \Bigl[ \exists y \left[ A(x,y) \land \forall y\prime \left( A(x,y\prime) \Rightarrow y = y\prime \right) \right] \land \\ && \forall x\prime \bigl[ \exists y\prime \left[ A(x\prime,y\prime) \land \forall y\prime\prime \left( A(x\prime,y\prime\prime) \Rightarrow y\prime = y\prime\prime \right) \right] \Rightarrow x = x\prime \bigr] \Bigr] \end{array} である。前者から後者は自明に導かれるが、その逆は成り立たない…と思う。