square root

Square roots


If KK is a monoid (which we write multiplicatively) and xx is an element of KK, then the element x 2x^2 is the square of xx. Conversely, if x 2=yx^2 = y, then xx is a square root of yy.

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

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

In constructive analysis

In constructive mathematics, we cannot prove that xx and x-x are the only square roots of x 2x^2. In the ordered field of real numbers, for example, the absolute value |x|{|x|} (like |x|-{|x|}, for that matter) is also a square root of x 2x^2, yet we cannot constructively prove that |x|=x{|x|} = x or |x|=x{|x|} = -x. Without using the lesser limited principle of omniscience, if xx is close to zero (and we do not yet know whether it is exactly zero), we cannot decide whether xx is nonnegative (so that |x|=x{|x|} = x) or nonpositive (so that |x|=x{|x|} = -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 2x^2, which is in fact |x|{|x|}. Thus, we can still use the notation y\sqrt{y}, but we cannot prove that every square root of yy is one of ±y\pm\sqrt{y}. However, we can prove, in any integral domain even, that if xyx \neq \sqrt{y} and xyx \neq -\sqrt{y}, then x 2yx^2 \neq y. (We are using the weak notions of field and integral domain so that \mathbb{R} will be an example.)

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

y|y|+y2+|y|y2i \sqrt{y} \coloneqq \sqrt{\frac{{|y|} + y}2} + \sqrt{\frac{{|y|} - y}2}\mathrm{i}

to construct a square root of yy. However, we cannot prove that every complex number has a square root in the internal language of an arbitrary 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 :U\sqrt{}\colon U \to \mathbb{C} for UU any neighbourhood of 00 in \mathbb{C}. This is important for interpreting the quadratic formula.

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

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


Revised on December 24, 2016 00:06:23 by Todd Trimble (