Given a claim with a uniqueness quantifier $\exists$!, such as: $$\forall x \exists!y \ P(x,y) $$
A standard translation that uses $\forall$ and $\exists$ only (there are several possible ones) is:
$$\forall x \exists y \ \big(P(x,y) \wedge \forall z(P(x, z) \supset z = y )\big)$$
I have two questions. The first involves expanding the predicate. If instead we have a three-place predicate and a repeated variable: $$\forall x \exists!y \ P(x,y,y) $$
is this a sound translation?
$$\forall x \exists y \big(P(x,y,y) \wedge \forall z(P(x,z,z) \supset z = y )\big) $$
... or do would I need to split up the $z$s like this?
$$\forall x \exists y \big(P(x,y,y) \wedge \forall u \forall v(P(x,u,v) \supset u = v \wedge v= y ) \big) $$
This seems like it covers more cases than it needs to, given that the $P(x,y,y)$ term on the left already eliminates cases where $u \not= v$.
My real question involves a more general algorithm for generating translations in cases of this sort. Given metavariables $\alpha, \beta, \delta$ that can stand for either $x$ or $y$, suppose we have a formula of this sort: $$\forall x \exists!y \ P(\alpha, \beta, \delta) $$
is this a sound method of generating a translation?
first, write "$\forall x \exists y \big( P(\alpha, \beta, \delta) \wedge \forall z(\ \ )\big)$"
then, inside the brackets after $\forall z$:
if $\alpha =y$, add "$(P(z, \beta, \delta) \supset z = y)$"
if $\beta =y$, add "$(P(\alpha, z, \delta) \supset z = y)$"
if $\delta =y$, add "$(P(\alpha, \beta, z) \supset z = y)$"
... with conjunction $\wedge$ between terms if you wind up with more than one, and replacing the metavariables with $x$ or $y$ as appropriate. Is this sound or have I missed the plot somewhere?
Consider your formula $\forall x \exists!y \ P(x,y,y)$, and suppose that we could rewrite it like this:
\begin{align} &\forall x \\ &\quad \text{let }\Phi(\alpha) = P(x,\alpha,\alpha) \text{ in}\\ &\quad \exists! y\ \Phi(y) \end{align}
Then, your transcription should generate something like this:
\begin{align} &\forall x \\ &\quad \text{let }\Phi(\alpha) = P(x,\alpha,\alpha) \text{ in}\\ &\quad \exists y\ \Big(\Phi(y) \land \forall z\ \Phi(z) \to z = y\Big) \end{align}
and then after inlining $\Phi$ you get the desired result.
In this light $$\forall x \exists y \big(P(x,y,y) \wedge \forall u \forall v(P(x,u,v) \supset u = v \wedge v= y ) \big) \tag{$\clubsuit$}$$ is not equivalent to $$\forall x \exists!y \ P(x,y,y).\tag{$\spadesuit$}$$ Consider $\Omega = \{0,1\}$ and $P = \{(0,0,0),(0,0,1),(1,1,0),(1,1,1)\}$, then $(\clubsuit)$ is false, while $(\spadesuit)$ is true.
I hope this helps $\ddot\smile$