20
$\begingroup$

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.

$\endgroup$
  • 3
    $\begingroup$ @WillSawin That isn't enough. It is possible to prove that every complex number has a square root in spite of the fact that there is no continuous function that gives the square root $\endgroup$ – jkabrg Sep 19 at 18:26
  • 2
    $\begingroup$ Showing that every complex number has a square root is already non-constructive, so in particular it is non-constructive for quaternion as well. This is due to the fact that it is not possible to chose the square root of $z \in \mathbb{C}$ continuously near every point (it do not work around $0$). One can show constructively that every Quaternion $q$ such that $N(q)>0$ has a square root though. $\endgroup$ – Simon Henry Sep 19 at 18:43
  • 4
    $\begingroup$ @SimonHenry: the fundamental theorem of algebra holds constructively, dx.doi.org/10.2140/pjm.2000.196.213 In particular, the polynomial $z^2 - c = 0$ has a root, for all $c \in \mathbb{C}$. $\endgroup$ – Andrej Bauer Sep 19 at 18:48
  • 2
    $\begingroup$ You used excluded middle: either $v = 0$ or $v \neq 0$. $\endgroup$ – Andrej Bauer Sep 19 at 19:09
  • 4
    $\begingroup$ @CarloBeenakker asked whether the proof he linked to was constructive. My point was that already the first step, namely assuming every quaternion has the form $a + b u$ for unit $u$ is problematics, constructively. That's why we're discussing constructive math. $\endgroup$ – Andrej Bauer Sep 19 at 19:20
13
$\begingroup$

Reduction to LLPO (Lesser Limited Principle of Omniscience).

The statement LLPO is the following (from Wikipedia): For any sequence a0, a1, ... such that each ai is either 0 or 1, and such that at most one ai is nonzero, the following holds: either a2i = 0 for all i, or a2i+1 = 0 for all i, where a2i and a2i+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.

$\endgroup$
  • 3
    $\begingroup$ This seems very nice, and much cleaner than the type 2 computability argument! $\endgroup$ – Peter LeFanu Lumsdaine Sep 20 at 8:16
6
$\begingroup$

([edit] The discussion between me and Andrej refers to an earlier version of the argument, which was more confusing than this one)

The operation is not Type 2 computable. The argument is similar to how the set $\mathbb R$ is not computably equivalent to its decimal representation. This latter statement is called the tablemaker's dilemma. Constructivists and Type 2 computability theorists make use of a redundant "nega-binary" representation of real numbers instead.

Let $q=-1 + 0i + 0j + 0k$. Assume the T2TM (Type 2 Turing Machine) outputs a quaternion $r$. This $r$ is a vector. Now observe that the machine must have read only finitely many digits of the nega-binary representation of $q$. Displace $q$ by some vector $v$ which is not parallel to $r$, where the vector $v$ has magnitude smaller than $2^{-n}$, where $n$ is the number of nega-binary digits the machine has read. The machine must give the same output because the prefix of the new input is the same, but this output is wrong.

To demonstrate that two quaternions very close to $-1$ may have very different square roots: Consider $-1 + \epsilon i$: Its square roots are $\pm (i + \frac{\epsilon}2)+ o(\epsilon)$. Now consider $-1 + \delta j$: Its square roots are $\pm (j + \frac{\delta}2)+ o(\delta)$. Now the distance between each of each of these sets is at least $\sqrt{2}$, which is much greater than zero. If after reading $n$ digits of $q = -1.0 + 0i + 0j + 0k$, the machine decides to output the first digits of $0 + 1i + 0j + 0k$, then one can play a trick on it by changing $q$ to $q' = -1 + 0i + 10^{-2n}j + 0k$. Those first digits of the output will then be completely wrong.

This T2TM argument is probably a valid Type 1 argument. In which case, it provides a convincing proof that quaternion square-root is uncomputable, and therefore can not be proved constructively.

It would be nice to see a "purer" proof that reduces to LPO or some other such principle, but I can't think of one. [edit] See below.

$\endgroup$
  • 1
    $\begingroup$ You're trying to show there is no computable function which respects equality and computes square roots. That's not what Type II computability does in such situations, they instead consider multi-valued representations, i.e., the answer may depend on the representation of the input (so that different representations of the same number may yield different square roots). $\endgroup$ – Andrej Bauer Sep 19 at 18:31
  • 1
    $\begingroup$ You may use a continuity argument, but you have to use it on the space of representations (the Baire space), not the quaternions. Anyhow, this looks constructive to me, but I have to learn first how to compute square roots of quaternions. $\endgroup$ – Andrej Bauer Sep 19 at 18:36
  • 2
    $\begingroup$ Here's a simpler example: for each real we can compute an integer larger than it (but depending on the representations), even though we cannot compute an integer larger than the real in a way that respects equality of reals. $\endgroup$ – Andrej Bauer Sep 19 at 18:37
  • 1
    $\begingroup$ Let us continue this discussion in chat. $\endgroup$ – jkabrg Sep 19 at 18:38
  • 1
    $\begingroup$ @AndrejBauer My argument is in the space of representations $\endgroup$ – jkabrg Sep 19 at 18:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.