[proofplan]
We reduce the defining formula to a quantifier-free Boolean combination of polynomial equalities and inequalities by quantifier elimination for real closed fields. The finitely many polynomials appearing in that quantifier-free formula have only finitely many roots, and those roots cut the ordered field into finitely many points and open intervals. On each such open interval every relevant polynomial has constant sign, so the truth value of the Boolean combination is constant there; the definable set is therefore a union of some of those intervals together with some of the root points.
[/proofplan]
[step:Replace the defining formula by a quantifier-free polynomial sign condition]
Let $A \subset F$ be definable with parameters from $F$. Then there is an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x,b)$, where $x$ is one free variable and $b=(b_1,\dots,b_s) \in F^s$ is a parameter tuple, such that
\begin{align*}
A = \{x \in F : F \models \varphi(x,b)\}.
\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,b)$ such that, for every $x \in F$,
\begin{align*}
F \models \varphi(x,b) \iff F \models \psi(x,b).
\end{align*}
After evaluating the parameters $b_1,\dots,b_s$, the formula $\psi(x,b)$ is a Boolean combination of atomic formulas of the form
\begin{align*}
p(x)=0,\qquad p(x)>0,\qquad p(x)<0,
\end{align*}
where each $p \in F[X]$ is a polynomial in one variable with coefficients in $F$.
Let $p_1,\dots,p_r \in F[X]$ be the finite list of all nonzero polynomials appearing in these atomic formulas. Constant zero polynomials may be removed from the list because each atomic formula involving such a polynomial has a fixed truth value independent of $x$.
[guided]
Since $A$ is definable with parameters from $F$, we can choose a formula $\varphi(x,b)$ with one free object variable $x$ and a fixed parameter tuple $b=(b_1,\dots,b_s) \in F^s$ such that
\begin{align*}
A = \{x \in F : F \models \varphi(x,b)\}.
\end{align*}
The purpose of quantifier elimination is to replace arbitrary first-order complexity by direct polynomial sign information. The theory of real closed fields admits quantifier elimination, so there is a quantifier-free formula $\psi(x,b)$ equivalent to $\varphi(x,b)$ over $F$:
\begin{align*}
F \models \varphi(x,b) \iff F \models \psi(x,b)
\end{align*}
for every $x \in F$.
Once the parameters $b_1,\dots,b_s$ are fixed elements of $F$, every term in one variable is represented by a polynomial in $F[X]$. Therefore $\psi(x,b)$ is a Boolean combination of finitely many atomic polynomial sign conditions
\begin{align*}
p(x)=0,\qquad p(x)>0,\qquad p(x)<0.
\end{align*}
Let $p_1,\dots,p_r \in F[X]$ be the finite list of all nonzero polynomials that occur in those atomic conditions. If a zero polynomial occurs, its sign condition is already either always true or always false, so it contributes no subdivision of $F$.
[/guided]
[/step]
[step:Cut the line by the roots of the finitely many polynomials]
For each index $i \in \{1,\dots,r\}$, define the root set
\begin{align*}
Z_i := \{a \in F : p_i(a)=0\}.
\end{align*}
Because $p_i$ is a nonzero one-variable polynomial over the field $F$, the set $Z_i$ is finite and satisfies
\begin{align*}
|Z_i| \leq \deg p_i.
\end{align*}
Define the finite set of all relevant roots by
\begin{align*}
Z := \bigcup_{i=1}^r Z_i.
\end{align*}
List the distinct elements of $Z$ in increasing order as
\begin{align*}
c_1 < c_2 < \cdots < c_m.
\end{align*}
If $Z=\varnothing$, take $m=0$ and omit the list.
The set $F \setminus Z$ is the disjoint union of the following finitely many open intervals:
\begin{align*}
(-\infty,c_1),\quad (c_1,c_2),\quad \dots,\quad (c_{m-1},c_m),\quad (c_m,+\infty),
\end{align*}
with the evident interpretation when $m=0$.
[guided]
The only places where a polynomial sign condition can change are roots of the relevant polynomial. For each polynomial $p_i$, define
\begin{align*}
Z_i := \{a \in F : p_i(a)=0\}.
\end{align*}
A nonzero polynomial over a field has at most its degree many roots, so each $Z_i$ is finite. Since there are only finitely many polynomials, their union
\begin{align*}
Z := \bigcup_{i=1}^r Z_i
\end{align*}
is finite.
We now use the order on $F$. Write the distinct elements of $Z$ in increasing order:
\begin{align*}
c_1 < c_2 < \cdots < c_m.
\end{align*}
These points divide the line into finitely many open intervals:
\begin{align*}
(-\infty,c_1),\quad (c_1,c_2),\quad \dots,\quad (c_{m-1},c_m),\quad (c_m,+\infty).
\end{align*}
If there are no roots at all, then the single interval is $(-\infty,+\infty)=F$. This finite decomposition is the candidate cell decomposition.
[/guided]
[/step]
[step:Show every polynomial has constant sign on each complementary interval]
Let $J \subset F \setminus Z$ be one of the open intervals listed above. Fix $i \in \{1,\dots,r\}$. Since $J \cap Z_i = \varnothing$, the polynomial $p_i$ has no root in $J$.
We claim that $p_i$ has constant sign on $J$. Suppose otherwise. Then there exist $u,v \in J$ with $u<v$ such that $p_i(u)$ and $p_i(v)$ have opposite signs. Since $F$ is real closed, polynomials over $F$ satisfy the intermediate value property: if a polynomial takes values of opposite sign at two ordered points, then it has a root between them. Hence there exists $w \in F$ with
\begin{align*}
u < w < v
\end{align*}
and
\begin{align*}
p_i(w)=0.
\end{align*}
Because $J$ is an interval and $u,v \in J$, we have $w \in J$, contradicting $J \cap Z_i = \varnothing$. Thus $p_i$ is either always positive on $J$ or always negative on $J$.
[guided]
Fix one of the complementary intervals $J$. By construction, $J$ contains no root of any polynomial $p_i$. We must show more than nonvanishing: we need the sign of each $p_i$ to be constant throughout $J$.
Fix an index $i$. Assume, toward a contradiction, that $p_i$ does not have constant sign on $J$. Since $p_i$ never vanishes on $J$, this means there are points $u,v \in J$ with $u<v$ such that $p_i(u)$ and $p_i(v)$ have opposite signs.
Here we use the real closedness of $F$. Over a real closed field, one-variable polynomials satisfy the intermediate value property: a polynomial that changes sign between two ordered points has a zero between those points. Applying this to $p_i$ on the ordered pair $u<v$, there exists $w \in F$ such that
\begin{align*}
u < w < v
\end{align*}
and
\begin{align*}
p_i(w)=0.
\end{align*}
Since $J$ is an interval and both endpoints $u$ and $v$ lie in $J$, the intermediate point $w$ also lies in $J$. But then $w \in J \cap Z_i$, contradicting the construction of $J$ as disjoint from all roots in $Z_i$. Therefore $p_i$ has constant sign on $J$.
[/guided]
[/step]
[step:Conclude that the formula is constant on each cell]
Let $J$ be one of the open intervals in $F \setminus Z$. For every $i \in \{1,\dots,r\}$, the truth values of
\begin{align*}
p_i(x)=0,\qquad p_i(x)>0,\qquad p_i(x)<0
\end{align*}
are independent of $x \in J$: the equality is always false, and the two strict inequalities are determined by the constant sign of $p_i$ on $J$. Since $\psi(x,b)$ is a Boolean combination of these finitely many atomic formulas, the truth value of $\psi(x,b)$ is constant on $J$.
At each point $c_k \in Z$, the truth value of $\psi(c_k,b)$ is a single fixed Boolean value. Therefore $A$ is obtained by selecting some of the finitely many open intervals in $F \setminus Z$ and some of the finitely many points $c_1,\dots,c_m$:
\begin{align*}
A = \{c_k : 1 \leq k \leq m,\ F \models \psi(c_k,b)\}
\cup
\bigcup_{\substack{J \text{ a component of } F \setminus Z\\ F \models \psi(x,b)\text{ for some, equivalently every, }x \in J}} J.
\end{align*}
This is a finite union of points and intervals with endpoints in $F \cup \{-\infty,+\infty\}$, as required.
[/step]
