Is the square root axiom redundant in the standard set of axioms for real closed fields?

Question

Real closed fields, that is, ordered fields $(F;+,-,*,0,1,<)$ which are elementarily equivalent to the ordered field of the real numbers, can be axiomatized by the standard axioms for ordered fields, along with an axiom stating that every positive element has a square root, along with an axiom schema stating that every odd-degree polynomial has a root. I am wondering whether the second item is redundant. I suspect it is not, and I want to see the construction of an ordered field where every odd-degree polynomial has a root, but where not every positive element has a square root. Or is the square root axiom in fact redundant?

Answer 1

Start with $\mathbb{Q}$ and repeatedly adjoin real roots of irreducible polynomials of odd degree by transfinite recursion until it is no longer possible to do so. The resulting field $F\subset\mathbb{R}$ will have the property that every finitely generated subfield has odd degree over $\mathbb{Q}$, and so in particular $\sqrt{2}\not\in F$. Every odd degree polynomial over $F$ has a root, since it must have some irreducible factor of odd degree, and then that irreducible factor can only be linear since otherwise we would have adjoined a root of it in the construction of $F$.

(Actually, the transfinite recursion can be avoided, since by a suitable dovetailing construction you can arrange that every polynomial of odd degree gets handled within the first $\omega$ steps.)