Predicate Logic - How to define uniqueness

Question

"Every positive real number has a unique positive real square root."

\begin{align} \forall x ( (x\in\mathbb R\text{ ^ } x > 0) = > \exists y (y\in\mathbb R\text{ ^ } y > 0 \text{ ^ } y = \sqrt x )) \end{align}

Sorry for the terrible formatting, new to this.

I know I can express uniqueness using this.

\begin{align} \exists ! \end{align}

But how would I do it without it?

Answer 1

$\forall x\left[\left[x\in\mathbb{R}\wedge x>0\right]\Rightarrow\exists y\left[y\in\mathbb{R}\wedge y>0\wedge y^{2}=x\wedge\forall z\left[\left[z\in\mathbb{R}\wedge z>0\wedge z^{2}=x\right]\Rightarrow z=y\right]\right]\right]$

In words:

for every positive real $x$ there exists a positive real $y$ such that $y^2=x$ and such that every positive real $z$ that satisfies $z^2=x$ equalizes $y$.

Answer 2

The uniqueness condition must be expressed :

$\exists y (P(y) \land \forall x (P(x) \rightarrow x = y))$.

This is abbreviated as :

$\exists !yP(y)$.

For :

$∃!y(y∈R \land y>0 \land y= \sqrt x)$

we have :

$∃y[(y∈R \land y>0 \land y= \sqrt x) \land \forall z((z∈R \land z>0 \land z= \sqrt x) \rightarrow z=y)]$.