nLab
square root

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 $\pm \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 $\pm \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[\mathrm{i}]$ 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[\mathrm{i}]$ 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.

Related concepts

• root

• square root

• root of unity

References

• Fred Richman; 1998; The fundamental theorem of algebra: a constructive development without choice; Fred Richman’s Documents