Solution (source code)

= Solution

Let $f\in\mathbb R(X_1,\ldots,X_n)$ be positive semidefinite. The assertion that $f(x)\geq0$ wherever its denominator is nonzero is first-order in ordered fields and holds in $\mathbb R$. Since RCF is model-complete, it holds in every real closed extension of $\mathbb R$.

If $f$ were not a sum of squares, the Artin-Schreier ordering criterion would give an ordering of $\mathbb R(X_1,\ldots,X_n)$ in which $f<0$. Its real closure is a real closed extension of $\mathbb R$, contradicting the transferred assertion at the generic tuple $(X_1,ldots,X_n)$. Hence $f$ is a sum of squares. This is the <Model-theoretic proof of Hilbert's seventeenth problem>.