I have the following rules for rewriting sentences with bounded quantifiers in arbitrary first-order languages to ordinary (unbounded) quantifiers:
$$\begin{align}
\forall\phi(x).\psi(x)&\qquad\to\qquad\forall x.\phi(x)\implies \psi(x),\\
\exists\phi(x).\psi(x)&\qquad\to\qquad\exists x.\phi(x)\land\psi(x)
\end{align}$$
… where $\phi$ and $\psi$ are formulae with free variable $x$ ($\phi$ is the scope of the quanitfier – e.g. $\forall x\in\Bbb{R}.\psi(x)$).
Additionally, I have…
$$\exists!x.\phi(x)\qquad\to\qquad \exists x.\forall y.\phi(y)\iff y=x$$
I would like to expand bounded uniqueness quantifiers in arbitrary first-order languages. (i.e. $\exists!\phi(x).\psi(x)$) in the same way as the universal and existential quantifier.
As far as I can tell, there are two ways to do this, depending on whether I apply the rule for expanding the existential or uniqueness quantifier first (provided that these rules are appropriately modified).
Applying the rule for existential quantifiers first yields the sequence of reductions:
$$\begin{align}
\exists!\phi(x).\psi(x)&\qquad\to\qquad\exists!x.\phi(x)\land\psi(x)\\
&\qquad\to\qquad\exists x.\forall y.(\phi(y)\land\psi(y))\iff y=x&(\textbf{fmla 1})
\end{align}$$
Applying the rule for uniqueness quantifiers first yields:
$$\begin{align}
\exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\forall\phi(y).\psi(y)\iff y=x\\
&\qquad\to\qquad\exists \phi(x).\forall y.\phi(y)\implies(\psi(y)\iff y=x)\\
&\qquad\to\qquad\exists x.\phi(x)\land\forall y.\phi(y)\implies(\psi(y)\iff y=x)&(\textbf{fmla 2})
\end{align}$$
Analytic tableaux shows that these are nonequivalent if $=$ is taken only to be an equivalence relation.
The ncatlab page on quantifiers provides the following:
$$\exists!\, x\colon T, P(x) \;\equiv\; \exists\, x\colon T, P(x) \wedge \forall\, y\colon T, P(y) \Rightarrow (x = y)$$
…which, generalizing the typing relation to arbitrary formulae, would suggest…
$$\begin{align}
\exists!\phi(x).\psi(x)&\qquad\to\qquad\exists\phi(x).\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\
&\qquad\to\qquad\exists x.\phi(x)\land\psi(x)\land\forall\phi(y).\psi(y)\implies y=x\\
&\qquad\to\qquad\exists x. \phi(x)\land\psi(x)\land\forall y.\phi(y)\implies(\psi(y)\implies y=x) & (\textbf{fmla 3})
\end{align}$$
This is most similar to formula 2, but weaker due to the replacement of the bi-implication $\psi(y)\iff y=x$ with the implication $\psi(y)\implies y=x$. Analytic tableaux shows that $\textbf{fmla 2}\implies\textbf{fmla 3}$ if $=$ is taken to be an arbitrary equivalence relationship.
Countermodels
These were obtained via analytic tableaux using the program found here (github here)
Define:
$E:=\forall x.\forall y.\forall z.R(x,x)\land(R(x,y)\implies R(y,x))\land((R(x,y)\land R(y,z))\implies R(x,z))$
(i.e. $R$ is an equivalence relation)
For $E\implies (\textbf{fmla 1}\implies\textbf{fmla 2})$ the program timed-out
$E\implies (\textbf{fmla 1}\implies\textbf{fmla 3})$ is valid
For $E\implies (\textbf{fmla 2}\implies\textbf{fmla 1})$ we have the countermodel $\mathcal{M}_1:=\langle D=\{0,1\}, R=D^2,\ \phi=\{0\},\ \psi=\{0,1\}\rangle$
$E\implies (\textbf{fmla 2}\implies \textbf{fmla 3})$ is valid
For $E\implies (\textbf{fmla 3}\implies \textbf{fmla 1})$, we have the countermodel $\mathcal{M}_2:=\langle D=\{0,1\},R=D^2,\ \phi=D,\ \psi=\{0\}\rangle$
For $E\implies (\textbf{fmla 3}\implies \textbf{fmla 2})$, we have the countermodel $\mathcal{M}_2$
Best Answer
The three formulations are all equivalent. The last one is the most intuitive variant and can be shortened in two steps to the first variant by essentially incorporating the $\phi$ and $\psi$ predications on $x$ into the $\forall y$ clause, by making the implication two-directional and saying that $\phi$ and $\psi$ must also hold if the object currently consiered is $x$. One may also "unsimplify" and go in the other direction from the first over the second to the third.
(1) and (2):
Transforming the biimplication into a conjunction of two implication directions:
$A \to (B \to C)$ is logically equivalent to $(A \land B) \to C$, which gives the equivalence of the $\Longrightarrow$ direction of the biimplication, $𝜙(𝑦)∧𝜓(𝑦) \Longrightarrow 𝑦=𝑥$ and $𝜙(𝑦)⟹(𝜓(𝑦) \Rightarrow 𝑦=𝑥)$.
The $\Longleftarrow$ direction can be obtained from (2) to (1) with $\phi(x) \land \ldots $ and $y = x$ by substituting $y$ for $x$ to obtain $\phi(y) \land \ldots $, thereby "importing" the $\psi(x)$ into the $\forall y$ clause. In the other direction from (1) to (2) one may likewise "export" and explicity specify $\phi(x)$, thereby resolving the dependency on $y = x$ and weakening the biimplication to a one-directional implication.
(2) and (3):
Analagous to above, by exporting the predication of $\psi$ on $x$ into a separate clause, the biimplication can be weakend to just the $\Rightarrow$ direction because now $\psi(x)$ is captured by an explicit predication and can do without the combination $\psi(y)$ and $y = x$.
Strenthening the implication to a biimplication with $x = y$ and substituting $y$ for $x$ makes it possible to go in the other direction and import the $\psi(x)$ into the $\forall$ clause.
(1) and (3) follows by transitivity.
I sketched these results with natural deduction proofs and was able to confirm the interderivability of all three; something must have gone wrong in your tableaus -- perhaps the treatment of the equality symbol?
Re. your counter models:
$M_1$ is not a counter model of (2) $\vDash$ (1) because it is not a model of (2) because $v(x) = 0$ is the only $x$ such that $\phi(x)$, but for $v(y) = 1$ since $\psi(y)$ but not $y = x$ the biconditional is false and hence the formula is not true for all $y$.
$M_2$ is not a counter model of (3) $\vDash$ (1) because it is a model of (1) because with $v(x) = 0$, for $v(y) = 0$, both the conjunction and the equality is true and for $v(y) = 1$, both the conjunction and the biconditional is false, and hence for all $y$ the formula is true.
$M_2$ is not a counter model of (3) $\vDash$ (2) analogously.