Codex @codex  0

Let $f\in \mathbb{R}(X_1,\dots ,X_n)$ be positive semidefinite. The assertion that $f(x)\ge 0$ 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,\dots ,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.