7
$\begingroup$

Is it possible to prove that every complex number has a square root using analytic LLPO, but avoiding Weak Countable Choice or Excluded Middle? Unique Choice is allowed.

(Analytic LLPO is the statement that given any pair of real numbers $x$ and $y$, either $x \leq y$ or $x \geq y$. This statement is non-constructive, but still weaker than other statements like LPO or Excluded Middle.)

It is true in Johnstone's Topological Topos. This is because the Fundamental Theorem of Algebra is true for Cauchy Real numbers, and Cauchy reals are isomorphic to Dedekind reals in the Topological Topos. But this reasoning doesn't seem to work unless Cauchy is iso to Dedekind.

$\endgroup$
0

1 Answer 1

7
$\begingroup$

Yes it is but there is no extensional square root function unless we also have LPO.

Note that the squaring function is a bijection from $Q_{+} = \{x + iy \mid x \geq 0, y \geq 0\}$ onto $H_{+} = \{x + iy \mid y \geq 0\}$. Similarly it is a bijection from $Q_{-} = \{x + iy \mid x \geq 0, y \leq 0\}$ onto $H_{-} = \{x + iy \mid y \leq 0\}$. Given LLPO, $H_{+} \cup H_{-} = \mathbb{C}$ and that is enough to prove the existence of square roots. The confusing part is that for a negative real number $x$, we obtain the square root $+ i\sqrt{-x}$ or $-i\sqrt{-x}$ depending on whether LLPO gives $x \in H_{+}$ or $x \in H_{-}$. So this does not give an extensional square root function.

Interestingly, this argument gives the stronger conclusion that every complex number has a square root in $$Q_{+} \cup Q_{-} =\{ x + iy \mid x \geq 0\}. $$ This stronger statement turns out to be equivalent to LLPO. Indeed, given a small enough real number $x$, if the square root of $-1+ix$ in $Q_{+} \cup Q_{-}$ is close to $i$ then $x \geq 0$ and similarly if that square root is close to $-i$ then $x \leq 0$.

$\endgroup$
4
  • $\begingroup$ Do you have a reference to fill in the gap of that last sentence? $\endgroup$
    – cody
    Feb 25, 2020 at 14:35
  • $\begingroup$ @cody The gap? What am I missing? $\endgroup$ Feb 25, 2020 at 14:37
  • $\begingroup$ The fact that you need LPO to build an extensional square root function doesn't seem to obviously follow from this argument. $\endgroup$
    – cody
    Feb 25, 2020 at 14:42
  • 2
    $\begingroup$ @cody Ah, the other last sentence! That's basically from Grilliot's trick: an extensional square root function has to be discontinuous somewhere. $\endgroup$ Feb 25, 2020 at 14:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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