[proofplan] The forward direction is the content of quantifier elimination for real closed fields: any formula with parameters from $F$ is equivalent over $F$ to a quantifier-free ordered-ring formula. Quantifier-free ordered-ring formulas define exactly finite Boolean combinations of polynomial equalities and inequalities, because their atomic formulas are comparisons between polynomial terms. The reverse direction is obtained by reading any finite Boolean combination of polynomial sign conditions directly as an ordered-ring formula with coefficients from $F$ used as parameters. [/proofplan] [step:Translate semialgebraic descriptions into ordered-ring formulas] Assume first that $A \subset F^n$ is semialgebraic over $F$. By definition, there exist finitely many polynomials $p_1,\dots,p_m \in F[X_1,\dots,X_n]$ such that $A$ is obtained from sets of the form \begin{align*} Z_i &= \{x \in F^n : p_i(x)=0\},\\ P_i &= \{x \in F^n : p_i(x)>0\} \end{align*} by finitely many unions, intersections, and complements. For each $i \in \{1,\dots,m\}$, the polynomial $p_i$ determines an $\mathcal{L}_{\mathrm{or}}$-term $\tau_i(x_1,\dots,x_n)$ using the coefficients of $p_i$ as parameters from $F$. Then $Z_i$ is defined by the atomic formula $\tau_i(x)=0$, and $P_i$ is defined by the atomic formula $\tau_i(x)>0$. Since finite unions, intersections, and complements correspond respectively to disjunctions, conjunctions, and negations of formulas, the finite Boolean construction of $A$ gives an $\mathcal{L}_{\mathrm{or}}$-formula with parameters from $F$ defining $A$. Hence $A$ is definable in $F$ with parameters from $F$. [guided] We start from the semialgebraic description and turn it into syntax in the ordered-ring language. Since $A$ is semialgebraic over $F$, there are finitely many polynomials $p_1,\dots,p_m \in F[X_1,\dots,X_n]$ such that $A$ is built from the basic sign sets \begin{align*} Z_i &= \{x \in F^n : p_i(x)=0\},\\ P_i &= \{x \in F^n : p_i(x)>0\} \end{align*} using finitely many Boolean operations. For each polynomial $p_i$, its coefficients lie in $F$. Because parameters from $F$ are allowed, those coefficients may appear in an $\mathcal{L}_{\mathrm{or}}$-formula. Thus $p_i$ is represented by an ordered-ring term $\tau_i(x_1,\dots,x_n)$, obtained by writing $p_i$ using addition, subtraction, multiplication, the constants $0,1$, and the coefficient parameters from $F$. The set $Z_i$ is therefore defined by the atomic formula $\tau_i(x)=0$, while $P_i$ is defined by the atomic formula $\tau_i(x)>0$. Now we match set operations with logical connectives. If formulas $\alpha(x)$ and $\beta(x)$ define sets $B,C \subset F^n$, then $\alpha(x)\lor\beta(x)$ defines $B\cup C$, $\alpha(x)\land\beta(x)$ defines $B\cap C$, and $\neg\alpha(x)$ defines $F^n\setminus B$. Since the semialgebraic description of $A$ uses only finitely many such operations, it produces a single finite $\mathcal{L}_{\mathrm{or}}$-formula with parameters from $F$ defining $A$. Thus $A$ is definable in $F$ with parameters from $F$. [/guided] [/step] [step:Eliminate quantifiers from a definable description] Conversely, assume that $A \subset F^n$ is definable in the $\mathcal{L}_{\mathrm{or}}$-structure $F$ with parameters from $F$. Then there are a tuple of parameters $a \in F^r$, for some $r \in \mathbb{N} \cup \{0\}$, and an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x,a)$ with free object variables $x=(x_1,\dots,x_n)$ such that \begin{align*} A = \{x \in F^n : F \models \varphi(x,a)\}. \end{align*} By quantifier elimination for real closed fields (citing a result not yet in the wiki: Quantifier Elimination for Real Closed Fields), there is a quantifier-free $\mathcal{L}_{\mathrm{or}}$-formula $\psi(x,a)$ such that, for every $x \in F^n$, \begin{align*} F \models \varphi(x,a) \iff F \models \psi(x,a). \end{align*} Hence \begin{align*} A = \{x \in F^n : F \models \psi(x,a)\}. \end{align*} [guided] Now suppose $A$ is definable. This means that the membership condition for $A$ is given by a first-order formula in the ordered-ring language, possibly with parameters from $F$. Thus there are parameters $a \in F^r$, where $r \in \mathbb{N}\cup\{0\}$, and an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x,a)$ with free object variables $x=(x_1,\dots,x_n)$ such that \begin{align*} A = \{x \in F^n : F \models \varphi(x,a)\}. \end{align*} The obstacle is that $\varphi$ may contain quantifiers over $F$. A semialgebraic description, however, must be a finite Boolean combination of polynomial sign conditions in the visible variables $x_1,\dots,x_n$. This is exactly where quantifier elimination for real closed fields is used. Since $F$ is real closed, quantifier elimination for real closed fields applies to the $\mathcal{L}_{\mathrm{or}}$-structure $F$ and gives a quantifier-free formula $\psi(x,a)$ equivalent to $\varphi(x,a)$ over $F$; that is, for every $x \in F^n$, \begin{align*} F \models \varphi(x,a) \iff F \models \psi(x,a). \end{align*} Therefore replacing $\varphi$ by $\psi$ does not change the subset of $F^n$ being defined: \begin{align*} A = \{x \in F^n : F \models \psi(x,a)\}. \end{align*} The point of this replacement is that quantifier-free ordered-ring formulas have only Boolean structure on top of atomic polynomial comparisons, which is exactly the semialgebraic format. [/guided] [/step] [step:Read the quantifier-free formula as a finite Boolean combination of polynomial sign conditions] Because $\psi(x,a)$ is quantifier-free, it is built from finitely many atomic ordered-ring formulas by finitely many Boolean connectives. Each term appearing in such an atomic formula is a polynomial expression in $x_1,\dots,x_n$ with coefficients in $F$, since the only function symbols in $\mathcal{L}_{\mathrm{or}}$ are $+$, $-$, and $\cdot$, and the parameters $a$ lie in $F$. Thus every atomic formula in $\psi(x,a)$ has one of the forms \begin{align*} s(x,a)=t(x,a) \end{align*} or \begin{align*} s(x,a)<t(x,a), \end{align*} where $s(x,a)$ and $t(x,a)$ are polynomial terms. Defining $q=s-t \in F[X_1,\dots,X_n]$, these become respectively \begin{align*} q(x)=0 \end{align*} and \begin{align*} q(x)<0. \end{align*} The condition $q(x)<0$ is equivalent to $(-q)(x)>0$, with $-q \in F[X_1,\dots,X_n]$. Therefore every atomic formula in $\psi$ defines a basic semialgebraic set over $F$, and the Boolean connectives in $\psi$ give a finite Boolean combination of such sets. Hence $A$ is semialgebraic over $F$. [guided] We now inspect the quantifier-free formula $\psi(x,a)$. Since it has no quantifiers, it is a finite Boolean combination of atomic formulas. In the ordered-ring language, atomic formulas compare two terms: they have the form \begin{align*} s(x,a)=t(x,a) \end{align*} or \begin{align*} s(x,a)<t(x,a), \end{align*} where $s(x,a)$ and $t(x,a)$ are $\mathcal{L}_{\mathrm{or}}$-terms. What are such terms? The language has only the ring operations $+$, $-$, and $\cdot$, together with the constants $0$ and $1$. Since the extra symbols $a$ are parameters from $F$, every term $s(x,a)$ denotes a polynomial function in the variables $x_1,\dots,x_n$ with coefficients in $F$, and the same is true for $t(x,a)$. Therefore the difference $q=s-t$ is a polynomial in $F[X_1,\dots,X_n]$. The equality atom is exactly the polynomial equation \begin{align*} q(x)=0. \end{align*} The strict inequality atom is \begin{align*} q(x)<0, \end{align*} which is the same as \begin{align*} (-q)(x)>0. \end{align*} Since $-q \in F[X_1,\dots,X_n]$, this is one of the allowed basic polynomial positivity conditions. Finally, the Boolean connectives in $\psi$ translate into finite unions, intersections, and complements of the corresponding basic sets. Thus the set defined by $\psi$, and hence the original set $A$, is a finite Boolean combination of polynomial equalities and strict polynomial inequalities over $F$. This proves that $A$ is semialgebraic over $F$. [/guided] [/step] [step:Conclude the equivalence] The first step proves that every semialgebraic subset of $F^n$ is definable in the ordered-ring language with parameters from $F$. The second and third steps prove that every subset of $F^n$ definable in the ordered-ring language with parameters from $F$ is semialgebraic over $F$. Therefore the two classes of subsets of $F^n$ coincide. [/step]