Skip to main content
3 of 7
added 39 characters in body
wlad
  • 4.9k
  • 2
  • 21
  • 45

Every complex number has a square root from LLPO without Weak Countable Choice

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.

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.

wlad
  • 4.9k
  • 2
  • 21
  • 45