Expressing the statement "The equation $x^2 + 2x = 15$ has a unique solution." in formal language. Can the statement "The equation $x^2 + 2x = 15$ has a unique solution." be expressed in a form of the formal language as the following:
\begin{align*}
\exists x,\forall y,(((x^2 + 2x = 15)\wedge (y^2 +2x = 15)) \rightarrow (x=y))
\end{align*}
The universe is $\mathbb{N}$ for both $x$ and $y$.
 A: Personally, I read the English sentence "$F(x)=0$ has a unique solution" as synonymous with "$F(x)=0$ has exactly one solution", and therefore I would write your sentence as $$\exists x,(x^2+2x=15\land\forall y,(y^2+2y=15\to x=y))$$
and I would dismiss your answer as wrong because it means that there is some $x$ such that, for all $y$, either $x$ is not a solution or $y$ is not a solution or $x=y$. In other words, it's an unnatural way to state that either the equation has exactly one solution or there is an element that does not solve it.
As user Mauro ALLEGRANZA has pointed out, $$(\exists x, x^2+2x=15)\land(\forall y,\forall z,((y^2+2y=15\land z^2+2z=15)\to x=y))$$ is another reasonable formulation of the same concept of unique existence, which mimics the way several proofs of such statements are organized.
A: Not quite, even correcting for the minor typo. Let's generalise your statement a bit:
$$\exists x, \forall y (P(x) \land P(y) \implies (x = y))$$
This does not say that $P(x)$ is true for a unique $x$. Indeed, this statement is satisfied if there is some $x$ such that $\lnot P(x)$. If there is such an $x$, then $P(x) \land P(y)$ is false for any $y$, and hence the implication is vacuously true.
