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

[Joe Shipman]

It’s straightforward to show without choice that there is a computable ordered field where every odd degree polynomial has a root and nonnegative numbers have square roots. I think the failure of choice corresponding to Lauchli’s result would not be that there is no real closed field that satisfies all the definitions, but that a field which satisfied the same first order properties as the reals in the language of fields could not necessarily be ordered compatibly with the field operations (have to make infinitely many choices of which square root of each prime shall be the “positive” one).

— JS

Sent from my iPhone

> On Jan 5, 2020, at 1:27 AM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom