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

[Timothy Y. Chow]

In ZF, one cannot prove that the algebraic closure of Q (the rationals) is 
unique.  In fact, Lauchli has constructed an algebraic closure of Q which 
has no real-closed subfield.

But now suppose we just want to build *an* algebraic closure L of Q with 
all the properties we know and love, and don't care that there might exist 
"exotic" algebraic closures of Q that are not isomorphic to L.  Since N 
(the natural numbers) is given to us with a well ordering, it is 
straightforward to construct L without needing to invoke AC.

What about the Artin-Schreier theorem?  It seems straightforward to 
construct (a particular version of) the real algebraic numbers, but what 
about proving that they form a real-closed field?  Glancing at a proof of 
Artin-Schreier, I instinctively feel that AC is not needed for the 
specific example of Q, but in light of Lauchli's result, I am worried that 
I am 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

Tim