Expansions of dense linear orders

(For some details and references, see Chapter 1 of my notes.)

We fix a structure ${\cal M} = (M,<,\dots)$ such that $(M,<)$ is a dense linear order. An interval is a nonempty interval with endpoints in $M \cup
\{-\infty,+\infty\}$.

We consider ${\cal M}$ with its interval topology on $M$ and the corresponding product topologies on the cartesian powers $M^k$.

Example: Puiseux series

Let $P$ be the set of all Puiseux series, that is, series of the form $G(X) = X^{p/d} \cdot F(X^{1/d})$, where $F(X)$ is a formal power series with real coefficients, $d$ is a nonzero natural number and $p$ is an integer. For such series the number $({\rm ord}(F)+p)/d$ is called its order and denoted by ${\rm ord}(G)$, and the leading coefficient of $G$ is the coefficient ${\rm lc}(G)$ of the monomial $X^{{\rm ord}(G)}$ in the series $G$.

For Puiseux series $G$ and $H$, we define $G+H$ and $G \cdot H$ in the usual way. We set $G \lt 0$ if and only if ${\rm lc}(G) \lt 0$, and $G \lt H$ if and only if $G-H \lt 0$.

Fact
The structure $(P,\lt)$ is a dense linear order, and its expansion ${\cal P} := (P,\lt,+,\cdot)$ is a real closed ordered field.

For a proof of this fact, see for instance Section 2.6 in the book Algorithms in Real Algebraic Geometry, by Saugata Basu, Richard Pollack and Marie-Françoise Coste-Roy.

Here is the gist of this proof: to show that $P$ is a field, let $F$ be a nonzero Puiseux series. Then $F(X) = aX^r(1+\epsilon(X))$, where $a \in \mathbb{R}$ is nonzero, $r \in \mathbb{Q}$ and $\epsilon$ is a Puiseux series of strictly positive order; hence
$\displaystyle \frac1F(X) = \frac1a X^{-r} \frac1{1+\epsilon(X)} = \frac1a X^{-r} \left(\sum_{k=0}^\infty \epsilon(X)^k\right).$
To show that $P$ is real closed, we show that every positive Puiseux series is a square and that every odd-degree polynomial over $P$ has a root. The former is similar to the argument above, using the Taylor series of the real function $x \mapsto \sqrt{1+x}$; the latter is more involved and uses Newton’s method.

One interesting observation about this proof is that the intermediate value theorem, which can be used to prove that every odd-degree polynomial over $\mathbb{R}$ has a real root, is not available over $P$ as the following shows.

Exercise
Prove that $P$ does not have the least-upper-bound property and is totally disconnected.

This means that, in the general context of ${\cal M}$, we need to restrict our attention to definable sets.

Definition
A definable set $S \subseteq M^n$ is definably connected if $S$ is not disconnected by any two nonempty, definable, open subsets.

Exercises

1. Prove that the image of a definably connected, definable set
   under a definable, continuous map is definably connected.
2. Let $S,T \subseteq M^n$ be definable and definably connected,
   and assume that ${\rm cl} S \cap T \ne \emptyset$. Prove that $S \cup
   T$ is definably connected.

Definition
The structure ${\cal M}$ is definably complete if every definable subset of $M$ has a supremum in $M \cup \{-\infty,+\infty\}$.

By the least upper bound principle for $\mathbb{R}$, every expansion of $(\mathbb{R},\lt)$ is definably complete.

Exercises
Assume that ${\cal M}$ is definably complete.

1. Prove that every interval is definably connected.
2. Intermediate Value Theorem: Let $f,g:I \longrightarrow M$ be definable and continuous, with $I \subseteq M$ an interval, and
   assume that $f(x) \ne g(x)$ for $x \in I$. Prove that either
   $f(x) \gt g(x)$ for all $x \in I$, or $f(x) \lt g(x)$ for all $x \in
   I$.