[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*}[/step]

[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: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}}$.[/step]

[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: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$.[/step]

[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: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]