[FOM] Artin-Schreier for Q, without choice?

[Ingo Blechschmidt]

Dear Tim,

On Sat 04 Jan 2020 02:36:22 PM GMT, Timothy Y. Chow wrote:
> What about the Artin-Schreier theorem?  It seems straightforward to
> construct (a particular version of) the real algebraic numbers, but what

indeed, you can write down the (Cauchy or Dedekind, won't matter in the
end) real numbers, construct the complex numbers from them (as ordered
pairs), cut down to the algebraic complex numbers and finally separate
out those algebraic complex numbers whose imaginary part is zero.

> about proving that they form a real-closed field?  Glancing at a proof of

Yes, no choice of any form and not even the law of excluded middle are
required in order to verify facts such as the following:

* Any algebraic complex number is zero or apart from zero.
* Any algebraic complex number is rational or not.
* Any monic polynomial over the algebraic complex numbers has a zero in
  the algebraic complex numbers.
* Any monic polynomial of odd degree over the real algebraic numbers has
  a zero in the real algebraic numbers.
* In the field of real algebraic numbers, any number is a square or the
  negative of a square.
* Formally adjoining an imaginary unit to the field of real algebraic
  numbers yields a field which is isomorphic to the field of algebraic
  complex numbers.

A textbook reference is *A course in constructive algebra* by Mines,
Richman and Ruitenburg.

> missing some subtle point.  Also, in the absence of AC, do we need to be
> cautious about the precise statement of any of the usual properties of
> real-closed fields---such as those listed on Wikipedia?
> 
> https://en.wikipedia.org/wiki/Real_closed_field

I can confirm 2, 3, 4, 5 and 8 for the real algebraic numbers as
constructed above. I haven't thought about the others.

Cheers,
Ingo