[proofplan]
We prove the semantic formulation: any two real closed ordered fields satisfy the same $L_{\mathrm{or}}$-sentences. Quantifier elimination for real closed ordered fields reduces every sentence, modulo $\mathrm{RCF}$, to a quantifier-free sentence. Since a quantifier-free sentence has no free variables, it is a Boolean combination of equalities and inequalities between closed ordered-ring terms, and every such closed term denotes an integer multiple of $1$. The truth of these integer equalities and inequalities is the same in every ordered field, so the original sentence has the same truth value in all models of $\mathrm{RCF}$.
[/proofplan]
[step:Reduce an arbitrary sentence to a quantifier-free sentence]
Let $\varphi$ be an $L_{\mathrm{or}}$-sentence. By quantifier elimination for real closed ordered fields (citing a result not yet in the wiki: Quantifier Elimination for Real Closed Fields), there exists a quantifier-free $L_{\mathrm{or}}$-formula $\psi$ with the same free variables as $\varphi$ such that
\begin{align*}
\mathrm{RCF} \models \varphi \leftrightarrow \psi.
\end{align*}
Since $\varphi$ is a sentence, $\psi$ has no free variables; hence $\psi$ is a quantifier-free $L_{\mathrm{or}}$-sentence.
Thus, for every real closed ordered field $F$,
\begin{align*}
F \models \varphi \quad \Longleftrightarrow \quad F \models \psi.
\end{align*}
[guided]
Let $\varphi$ be an $L_{\mathrm{or}}$-sentence. The main model-theoretic input is quantifier elimination for real closed ordered fields: every $L_{\mathrm{or}}$-formula is equivalent, over the theory $\mathrm{RCF}$, to a quantifier-free formula with the same free variables. Applying this to the sentence $\varphi$, we obtain a quantifier-free $L_{\mathrm{or}}$-formula $\psi$ such that
\begin{align*}
\mathrm{RCF} \models \varphi \leftrightarrow \psi.
\end{align*}
Because $\varphi$ has no free variables, the equivalent formula $\psi$ also has no free variables. Therefore $\psi$ is not merely quantifier-free; it is a quantifier-free sentence.
This means that in every real closed ordered field $F$, the sentences $\varphi$ and $\psi$ have the same truth value:
\begin{align*}
F \models \varphi \quad \Longleftrightarrow \quad F \models \psi.
\end{align*}
So it is enough to prove that every quantifier-free $L_{\mathrm{or}}$-sentence has the same truth value in every real closed ordered field.
[/guided]
[/step]
[step:Identify closed ordered-ring terms with integers]
Let $t$ be a closed $L_{\mathrm{or}}$-term. We claim that there exists an integer $n_t \in \mathbb{Z}$ such that, for every ordered field $F$, the interpretation $t^F$ of $t$ in $F$ satisfies
\begin{align*}
t^F = n_t \cdot 1_F.
\end{align*}
This is proved by structural induction on $t$. The constants $0$ and $1$ correspond to $0$ and $1$. If $t = -s$, take $n_t = -n_s$. If $t = s_1 + s_2$, take $n_t = n_{s_1} + n_{s_2}$. If $t = s_1 \cdot s_2$, take $n_t = n_{s_1}n_{s_2}$. These clauses cover all closed terms in $L_{\mathrm{or}}$.
[guided]
A closed $L_{\mathrm{or}}$-term is built from the symbols $0$, $1$, unary minus, addition, and multiplication, with no variables. We prove by structural induction that such a term always denotes an integer multiple of the multiplicative identity.
For the base cases, the closed term $0$ denotes
\begin{align*}
0_F = 0 \cdot 1_F,
\end{align*}
and the closed term $1$ denotes
\begin{align*}
1_F = 1 \cdot 1_F.
\end{align*}
Thus the associated integers are $0$ and $1$.
For the inductive steps, suppose closed terms $s$, $s_1$, and $s_2$ have associated integers $n_s$, $n_{s_1}$, and $n_{s_2}$, meaning that in every ordered field $F$,
\begin{align*}
s^F &= n_s \cdot 1_F, \\
s_1^F &= n_{s_1} \cdot 1_F, \\
s_2^F &= n_{s_2} \cdot 1_F.
\end{align*}
If $t = -s$, then
\begin{align*}
t^F = -s^F = (-n_s)\cdot 1_F,
\end{align*}
so $n_t = -n_s$. If $t = s_1 + s_2$, then
\begin{align*}
t^F = s_1^F + s_2^F = (n_{s_1}+n_{s_2})\cdot 1_F,
\end{align*}
so $n_t = n_{s_1}+n_{s_2}$. If $t = s_1 \cdot s_2$, then
\begin{align*}
t^F = s_1^F s_2^F = (n_{s_1}n_{s_2})\cdot 1_F,
\end{align*}
so $n_t = n_{s_1}n_{s_2}$. These are exactly the term-forming operations of $L_{\mathrm{or}}$, so the induction proves the claim.
[/guided]
[/step]
[step:Show atomic closed formulas have field-independent truth values]
Let $F$ be an ordered field. Since $F$ is ordered, it has characteristic $0$, and the map
\begin{align*}
\iota_F: \mathbb{Z} &\to F \\
n &\mapsto n \cdot 1_F
\end{align*}
is an injective order-preserving ring homomorphism.
Let $s$ and $t$ be closed $L_{\mathrm{or}}$-terms, with associated integers $n_s,n_t \in \mathbb{Z}$. Then
\begin{align*}
F \models s = t
\quad \Longleftrightarrow \quad
n_s = n_t
\end{align*}
and
\begin{align*}
F \models s < t
\quad \Longleftrightarrow \quad
n_s < n_t.
\end{align*}
The right-hand sides are statements in the ordered ring $\mathbb{Z}$, so their truth values do not depend on $F$.
[guided]
Let $F$ be an ordered field. The ordered-field axioms imply that $1_F > 0_F$. Hence, for every positive integer $m$,
\begin{align*}
m \cdot 1_F = \underbrace{1_F + \cdots + 1_F}_{m \text{ summands}} > 0_F.
\end{align*}
In particular, no positive integer multiple of $1_F$ is equal to $0_F$, so $F$ has characteristic $0$.
Define the canonical integer embedding
\begin{align*}
\iota_F: \mathbb{Z} &\to F \\
n &\mapsto n \cdot 1_F.
\end{align*}
This map is a ring homomorphism by the definitions of integer multiples of $1_F$, it is injective because $F$ has characteristic $0$, and it is order-preserving because positive integers are sent to positive elements of $F$.
Now let $s$ and $t$ be closed $L_{\mathrm{or}}$-terms. By the previous step, there are integers $n_s,n_t \in \mathbb{Z}$ such that
\begin{align*}
s^F &= n_s \cdot 1_F, \\
t^F &= n_t \cdot 1_F.
\end{align*}
Therefore
\begin{align*}
F \models s = t
\quad \Longleftrightarrow \quad
n_s \cdot 1_F = n_t \cdot 1_F
\quad \Longleftrightarrow \quad
n_s = n_t,
\end{align*}
where the last equivalence uses injectivity of $\iota_F$. Similarly,
\begin{align*}
F \models s < t
\quad \Longleftrightarrow \quad
n_s \cdot 1_F < n_t \cdot 1_F
\quad \Longleftrightarrow \quad
n_s < n_t,
\end{align*}
where the last equivalence uses that $\iota_F$ preserves and reflects order. Thus every atomic closed formula has a truth value determined entirely by the corresponding statement about integers, independently of the ordered field $F$.
[/guided]
[/step]
[step:Pass from atomic formulas to quantifier-free sentences]
Every quantifier-free $L_{\mathrm{or}}$-sentence is obtained from atomic closed formulas of the forms $s=t$ and $s<t$ by finitely many Boolean operations. Since each atomic closed formula has the same truth value in every ordered field, induction on the Boolean construction of $\psi$ shows that $\psi$ has the same truth value in every ordered field.
In particular, if $K$ and $L$ are real closed ordered fields, then
\begin{align*}
K \models \psi \quad \Longleftrightarrow \quad L \models \psi.
\end{align*}
Using the equivalence of $\varphi$ and $\psi$ over $\mathrm{RCF}$ gives
\begin{align*}
K \models \varphi
\quad \Longleftrightarrow \quad
K \models \psi
\quad \Longleftrightarrow \quad
L \models \psi
\quad \Longleftrightarrow \quad
L \models \varphi.
\end{align*}
Thus $K$ and $L$ satisfy the same $L_{\mathrm{or}}$-sentences, so $K \equiv L$. Since $K$ and $L$ were arbitrary models of $\mathrm{RCF}$, the theory $\mathrm{RCF}$ is complete.
[/step]
