$F(\sqrt x \mid x > 0)$ is formally real In Jacobson's Basic Algebra IV, it is claimed in the proof of Theorem 8 page 285 that if $F$ is an ordered field then the extension $L = F(\sqrt x\mid x > 0)$ obtained by adjoining the square roots (taken e.g. in the algebraic closure) of each positive element is formally real. Why is this?
 A: Lemma: If $F$ is an ordered field and $x\in F$ is positive, then $F(\sqrt{x})$ may be equipped with an ordering extending that of $F$.
Proof: If $\sqrt{x}$ already lies in $F$ then the result is clear, so assume $\sqrt{x}\notin F$. Now, let $P$ be the set of positive elements of $F$, and define $Q\subseteq F(\sqrt{x})$ to be the set all sums of elements of $F(\sqrt{x})$ of the form $c^2p$, for some $c\in F(\sqrt{x})$ and some $p\in P$. We claim that $Q$ is a semi-positive cone, ie that $Q$ satisfies all the conditions to be a positive cone except perhaps that the condition that $F(\sqrt{x})=Q\cup Q^-$. Certainly $Q$ is closed under addition, and it is closed under multiplication since $P$ is closed under multiplication. Also, since $1\in P$, the square of every element of $F(\sqrt{x})$ lies in $Q$. Thus we need only show $-1\notin Q$.
Suppose otherwise that there exist some $c_i\in F(\sqrt{x})$ and $p_i\in P$ such that $c_1^2p_1+\dots+c_n^2p_n=-1$. Then, since every element of $F(\sqrt{x})$ is of the form $a+b\sqrt{x}$ for some $a,b\in F$, there are $a_i,b_i\in F$ such that each $c_i=a_i+b_i\sqrt{x}$. Expanding out the equation gives $$(a_1^2+b_1^2x)p_1+\dots+(a_n^2+b_n^2x)p_n+1=-2(a_1b_1p_1+\dots+a_nb_np_n)\sqrt{x}.$$ Now, if the coefficient of $\sqrt{x}$ on the right hand side were non-zero, then we could divide out by it and hence obtain $\sqrt{x}\in F$, a contradiction. So the right hand side must be zero, whence we must have $$(a_1^2+b_1^2x)p_1+\dots+(a_n^2+b_n^2x)p_n=-1$$ as well. This is a relation in the ordered field $F$, and by hypothesis we have $x>0$ and $p_i\geqslant 0$ (in F) for each $i$. Since the $a_i^2$ and $b_i^2$ are certainly non-negative, the left hand side is thus non-negative, contradicting the ordering of $F$.
So, $Q$ is indeed a semi-positive cone. Now, either $\sqrt{x}\in Q\cup Q^{-1}$ or not. In the latter case, by the argument here either $Q+Q\sqrt{x}$ or $Q+Q(-\sqrt{x})$ is a semi-positive cone, and we may thus assume that $\sqrt{x}\in Q\cup Q^-$. Note also that $P\cup P^-\subseteq Q\cup Q^-$. Since $Q$ is closed under addition and multiplication, and every element of $F(\sqrt{x})$ is of the form $a+b\sqrt{x}$ for some $a,b\in F=P\cup P^-$, this means that $F(\sqrt{x})=Q\cup Q^-$. So $Q$ is a positive cone and thus induces a total ordering on $F(\sqrt{x})$, and, since $Q\supseteq P$, this ordering extends the ordering on $F$, as desired.

Lemma: If $F$ is an ordered field and $x_1,\dots,x_n\in F$ are positive, then $F(\sqrt{x_1},\dots,\sqrt{x_n})$ may be equipped with an order extending that of $F$, and is hence formally real.
Proof: By induction on $n$ and the above lemma. Since the ordering of $F(\sqrt{x_1},\dots,\sqrt{x_{k-1}})$ at each step will extend that of $F$, we have in particular that $x_k$ is positive in $F(\sqrt{x_1},\dots,\sqrt{x_{k-1}})$, and so the hypothesis of the above lemma apply. $\blacksquare$

Now we can show the desired result. Suppose some $a_i\in L$ satisfy $a_1^2+\dots+a_k^2=0$. Since there are finitely many $a_i$, there are thus finitely many positive elements $x_j\in F$ such that each $a_i$ is of the form $$f(\sqrt{x_1},\dots,\sqrt{x_n})\big/g(\sqrt{x_1},\dots,\sqrt{x_n})$$ for some $F$-polynomials $f,g\in F[t_1,\dots,t_n]$. In particular, each of the $a_i$ lies in the field $F(\sqrt{x_1},\dots,\sqrt{x_n})$. But this field is formally real by the lemma above, and hence we must have $a_i=0$ for each $i\leqslant k$, as desired.
