# Square roots

## Definitions

If $K$ is a monoid (which we write multiplicatively) and $x$ is an element of $K$, then the element ${x}^{2}$ is the square of $K$. Conversely, if ${x}^{2}=y$, then $x$ is a square root of $y$.

If $K$ is an integral domain, then (in classical mathematics) $x$ and $-x$ are the only square roots of ${x}^{2}$. If $y$ has a square root, then we often denote its square roots together as $±\sqrt{y}$, although there is no meaning of $\sqrt{y}$ itself.

If $K$ is a linearly ordered field, then every element $y$ has a unique nonnegative square root if it has a square root at all; this is the principal square root of $y$ and denoted $\sqrt{y}$.

## In constructive analysis

In constructive mathematics, we cannot prove that $x$ and $-x$ are the only square roots of ${x}^{2}$. In the ordered field of real numbers, for example, the absolute value $\mid x\mid$ (like $-\mid x\mid$, for that matter) is also a square root of ${x}^{2}$, yet we cannot constructively prove that $\mid x\mid =x$ or $\mid x\mid =-x$. Without using the lesser limited principle of omniscience, if $x$ is close to zero (and we do not yet know whether it is exactly zero), we cannot decide whether $x$ is nonnegative (so that $\mid x\mid =x$) or nonpositive (so that $\mid x\mid =-x$).

However, in any linearly ordered field with an absolute value (including any real-closed field), we still have a unique nonnegative square root of ${x}^{2}$, which is in fact $\mid x\mid$. Thus, we can still use the notation $\sqrt{y}$, but we cannot prove that every square root of $y$ is one of $±\sqrt{y}$. However, we can prove, in any integral domain even, that if $x\ne \sqrt{y}$ and $x\ne -\sqrt{y}$, then ${x}^{2}\ne y$. (We are using the weak notions of field and integral domain so that $ℝ$ will be an example.)

If we accept results in the complex numbers (or in $K\left[\mathrm{i}\right]$ for $K$ any real-closed field), then every element of $K$ has a square root. Even if $y$ is close to zero, we can still use

$\sqrt{y}≔\sqrt{\frac{\mid y\mid +y}{2}}+\sqrt{\frac{\mid y\mid -y}{2}}\mathrm{i}$\sqrt{y} \coloneqq \sqrt{\frac{{|y|} + y}2} + \sqrt{\frac{{|y|} - y}2}\mathrm{i}

to construct a square root of $y$. However, we cannot prove that every complex number has a square root in the internal language of an aribtrary W-topos, although weak countable choice is enough to prove this. (See Richman (1998).) A counterexample is the topos of sheaves on the real line, since there is no continuous function $\sqrt{}:U\to ℂ$ for $U$ any neighbourhood of $0$ in $ℂ$. This is important for interpreting the quadratic formula.

How much choice is needed to prove that every element of $K\left[\mathrm{i}\right]$ has a square root, where $K$ is any real-closed field? Maybe COSHEP will do?

Note that there is never any trouble finding a square root of $y$ if we assume that $y\ne 0$, nor (obviously) is there any trouble if we assume that $y=0$. Accordingly, the classical results hold for discrete fields, but this doesn't apply constructively to analysis.

## References

Revised on December 1, 2010 06:12:44 by Toby Bartels (75.88.76.116)