The field of algebraic numbers exists constructively, since we can represent a number by an irreducible polynomial plus an estimate in rational coordinates that separates it from any other root.

More generally, if we have a countably enumerated field with decidable arithmetic, it seems like we can construct the algebraic closure by picking a countable ordering of the irreducible polynomials, then defining an ordering of the roots of each polynomial that respects the orderings chosen for all previous polynomials.


  1. Is it correct that something like this construction works for any constructive countable field?
  2. Is there a natural broader class of field for which the algebraic closure constructively exists?
  1. This is proved in Theorem VI.3.5 of "A Course in Constructive Algebra" by Ray Mines, Fred Richman, and Wim Ruitenburg.
  2. I'm not aware of any generalizations of this sort.
  • $\begingroup$ Would it generalize to any well ordered field? $\endgroup$ Jun 21 '20 at 21:48
  • $\begingroup$ It seems so, but I'm not sure. $\endgroup$ Jun 21 '20 at 21:56

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.