Model-theoretic proof of Hilbert's seventeenth problem (source code)

= Model-theoretic proof of Hilbert's seventeenth problem
{c}

Model completeness of real closed fields transfers positivity of a rational function from $\mathbb R$ to real closed extensions of $\mathbb R$. If the function were not a sum of squares, the Artin-Schreier ordering criterion would produce a real closure in which it is negative, giving a contradiction.