If is a monoid (which we write multiplicatively) and is an element of , then the element is the square of . Conversely, if , then is a square root of .
If is an integral domain, then (in classical mathematics) and are the only square roots of . If has a square root, then we often denote its square roots together as , although there is no meaning of itself.
If is a linearly ordered field, then every element has a unique nonnegative square root if it has a square root at all; this is the principal square root of and denoted .
In constructive mathematics, we cannot prove that and are the only square roots of . In the ordered field of real numbers, for example, the absolute value (like , for that matter) is also a square root of , yet we cannot constructively prove that or . Without using the lesser limited principle of omniscience, if is close to zero (and we do not yet know whether it is exactly zero), we cannot decide whether is nonnegative (so that ) or nonpositive (so that ).
However, in any linearly ordered field with an absolute value (including any real-closed field), we still have a unique nonnegative square root of , which is in fact . Thus, we can still use the notation , but we cannot prove that every square root of is one of . However, we can prove, in any integral domain even, that if and , then . (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 for any real-closed field), then every element of has a square root. Even if is close to zero, we can still use
to construct a square root of . 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 for any neighbourhood of in . This is important for interpreting the quadratic formula.
How much choice is needed to prove that every element of has a square root, where is any real-closed field? Maybe COSHEP will do?
Note that there is never any trouble finding a square root of if we assume that , nor (obviously) is there any trouble if we assume that . Accordingly, the classical results hold for discrete fields, but this doesn't apply constructively to analysis.