Is it possible to constructively prove that every $q \in \mathbb H$ has some $r$ such that $r^2 = q$? The difficulty here is that $q$ might be a negative scalar, in which case there might be "too many" values of $r$. Namely, $r$ could then equal any vector quaternion of magnitude $\sqrt{|q|}$. The presence of this seemingly severe discontinuity suggests that there can't be a way to constructively prove that every quaternion has a square root.


The variety of constructivism can be as strong as possible. So any Choice principle, or Markov's Principle, or Bar Induction, is allowed.


My thoughts were to do some kind of reduction to $LPO$ or $LLPO$ or $LEM$. But I don't see how.


The way to find a square-root classically is as follows: If $q = w + xi + yj + zk$ is not a scalar quaternion, then it lies on a unique "complex plane". This is due to the fact that a vector quaternion (of the form $xi + yj + zk$) always squares to $-(x^2 + y^2 + z^2)$, which is a negative scalar. The problem then reduces to finding the square root of a complex number. The difficulty is exactly in the case when $x=y=z=0$ and $w < 0$, in which case $q$ and $r$ lie on *all* complex planes.



Is it possible to constructively prove that every quaternion has a square root?
Reduction to LLPO (Lesser Limited Principle of Omniscience).


The statement LLPO is the following (from Wikipedia): For any sequence *a*0, *a*1, ... such that each *a**i* is either 0 or 1, and such that at most one *a**i* is nonzero, the following holds: either *a*2i = 0 for all *i*, or *a*2i+1 = 0 for all *i*, where *a*2i and *a*2i+1 are entries with even and odd index respectively. 


This is considered a quintessentially non-constructive claim.


The claim that every quaternion has a square root implies LLPO.


Consider a sequence $(p\_n)\_{n \geq 1} \in \{0,1\}$, with the property that *at most* one element of the sequence is equal to $1$. Consider the following infinite quaternionic series $q = -1 + i\left(1 - \sum\_{n=1}^\infty\frac{1 - p\_{2n}}{2^n}\right) + j\left(1 - \sum\_{n=1}^\infty\frac{1 - p\_{2n+1}}{2^n}\right)$. The series clearly converges. Now we assume that we can get an $r$ such that $r^2 = q$. Consider the angle $\theta$ between $r$ and $i$ (considered as 4d vectors with the standard inner product), and likewise consider the angle $\phi$ between $r$ and $j$. Either $\theta > \arctan(1/2)$ or $\phi > \arctan(1/2)$, as these two open regions cover all the non-zero quaternions. If $\theta > \arctan(1/2)$ then we conclude that all $p\_{2n}=0$. If $\phi > \arctan(1/2)$ then we conclude that all $p\_{2n+1}=0$. This is exactly LLPO.


