"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?
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)]$.
$\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$.
