Is it possible in constructive mathematics (no excluded middle or Axiom of Choice) to construct the algebraic numbers directly from the rationals (in say HoTT), without first constructing a real line and then augmenting it with the imaginary unit? In classical mathematics one could do this by appealing to the (obviously nonconstructive) principle that every field admits an algebraic closure.

One reason that I ask is that in constructive mathematics the real line seems a bit messy: the various constructions of the real line (Cauchy vs. Dedekind) are in general inequivalent without at least assuming countable choice, and in particular the usual construction of the Cauchy reals may not even be sequentially complete without countable choice (though the new higher-inductive type definition given in HoTT avoids this problem).

I'm relatively new to constructive mathematics, so I apologize if this construction is obvious (or obviously not possible).

Edit: I'm also curious about the constructive properties of the algebraic numbers, such as if they inherit decidable equality from the rationals?

  • 1
    $\begingroup$ I haven't read this yet, but this article may be interesting for you. $\endgroup$ – Mark Nov 29 '17 at 5:35
  • 1
    $\begingroup$ I would think you can just fix an enumeration of all polynomials with integer coefficients and inductively construct extensions where they split. But maybe there is some subtle issue with doing this constructively that I'm overlooking. $\endgroup$ – Eric Wofsey Nov 29 '17 at 6:05
  • $\begingroup$ @Eric: I think this basically just works, at least in ZF and requiring no choice; I don't know about in HoTT. See math.stackexchange.com/questions/114978/… for some discussion. $\endgroup$ – Qiaochu Yuan Nov 29 '17 at 7:06
  • $\begingroup$ @Mark thanks for the reference! Unfortunately it appears that they only discuss finite algebraic extensions of the rationals, rather than their algebraic closure consisting of all algebraic numbers. $\endgroup$ – ಠ_ಠ Nov 29 '17 at 22:50
  • 1
    $\begingroup$ the sum of a root of $x^2 - 2 = 0$ and a root of $x^2 - 8 = 0$ could be either a root of $x^2 - 2 = 0 $ or a root of $x^2 - 18 = 0$. $\endgroup$ – Daniel Schepler Nov 29 '17 at 23:27

Your Answer

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

Browse other questions tagged or ask your own question.