Recall that a structure on a set $S$ is a subset of $\bigcup_n \mathcal{P}(S^n)$ closed under products, Boolean operations, projection, containing singletons in $S$. This is a combinatorical shadow of what it means to do logic on $S$.
Definition 1. A structure on $\mathbb{R}$ is o-minimal when the only definable subsets of $\mathbb{R}$ are finite unions of points and intervals.
Tarski and Seidenberg proved that $\mathbb{R}_ \mathrm{alg}$ is o-minimal. Later Gabrielov showed that $\mathbb{R}_ \mathrm{an}$ is o-minimal, where this is the structure generated by $\mathbb{R}_ \mathrm{alg}$ and analytic functions on $[-1, 1]^n$. At this point, van den Dries defined o-minimality, and Wilkie showed that $\mathbb{R}_ \mathrm{exp}$ is o-minimal. Miller and van den Dries found a way to relativize this proof and show that $\mathbb{R}_ {\mathrm{an},\mathrm{exp}}$ is o-minimal. There is also a result that o-minimality is preserved by Pfaffian chains.
Remark 2. There is some growth dichotomy in o-minimal functions. A theorem of Miller says that if $S$ is an o-minimal structure on $\mathbb{R}$ but not polynomially bounded (i.e., there is a definable function that grows faster than any polynomial) then $S$ contains the real exponential $\exp$.
One can wonder about a trichotomy: polynomially bounded, structures “comparable” to $\mathbb{R}_ \mathrm{exp}$, transexponential growth. It is open whether there is an o-minimal structure with a transexponential function, i.e., one that grows faster than any tower of exponentials.
Strategies for proving o-minimality#
Definition 3. We say that a theory $T$ has elimination of quantifiers if the following holds: for all formulas $\varphi$ (with parameters) there exists a formula $\psi$ without quantifies such that $T \vdash (\varphi \leftrightarrow \psi)$.
For example, if $T$ is the theory of algebraically closed fields of characteristic zero, then this is essentially Chevalley’s theorem that says that the image of a constructible set under a projection is a constructible set.
Definition 4. We say that a theory $T$ is model-complete if every formula is equivalent to a universal formula (i.e., a formula with only universal quantifiers at the front).
Remark 5. Another way of thinking about it is that any embedding of models (i.e., the truth of primitive formula can be checked in the target) is elementary (i.e., the truth of all formulas can be checked in the target).
Another more useful way of thinking about it is that every definable set is the projection of a constructible set.
So using these notions, how do we prove o-minimality?
Strategy 6. Prove quantifier elimination.
Here, we need to understand having “quantifier elimination” really depends on the language rather than just the theory. For example, in $\mathbb{R}_ \mathrm{alg}$, is $\lbrace x \le y \rbrace$ definable by a primitive formula? It is definable as it can be written as $\exists z (y-x = z^2)$. But to write this using a quantifier free formula, we need to add the relation $\le$ to the language. So what we really want to do is to augment our language a “little bit” so that we do have quantifier elimination.
Strategy 7. Prove and use model-completeness.
If $S$ is model complete and $X \subseteq \mathbb{R}$ is definable, then we can write $X = \pi(Y)$ where $Y$ is constructible. So it is enough to show that constructible sets have finitely many connected components.
Example 8. For $\mathbb{R}_ \mathrm{an}$, Gabrielov has developed this notion of subanalytic sets. It follows from this theory that $\mathbb{R}_ \mathrm{an}$ is model-complete. Then we can use the second strategy.
Later, Defen and van den Dries had this idea of augmenting the language using $$ D = \lbrace (x, y, x/y) : \lvert x \rvert \le \lvert y \rvert \rbrace $$ and showed that this has quantifier elimination.
Quantifier elimination for $\mathbb{R}_ \mathrm{alg}$#
We give a proof that is circular, but can be fixed.
Lemma 9. Let $P(\bar{x}, y)$ be a polynomial where $\bar{x}$ is a tuple. Then there exists a “stratification by sign,” i.e., there are finitely many subsets $A_1, \dotsc, A_k \subseteq \mathbb{R}^n$ such that
- the sets $A_i$ are all constructible and form a partition,
- on each $A_i$ there exist finitely many continuous definable functions $\xi_\alpha(\bar{x})$ such that $P(\bar{x}, \xi_\alpha(\bar{x})) = 0$ are precisely all the zero, and the signs of $P(\bar{x}, y)$ between $\xi_\alpha$ are all fixed.
Once we have this, we get quantifier elimination. Indeed, because any quantifier free formula is a disjunctions of conjunctions, we just need to show that $$ \exists y (P_1(\bar{x}, y) \gt 0, P_2(\bar{x}, y) = 0, \dotsc) $$ is constructible. We induction on the degree $d$ of $P$ relative to $y$. When $d = 0$, this is easy. For $d \gt 0$, we consider the derivative $\partial P / \partial y$. By passing to a smaller constructible set $A \subseteq \mathbb{R}^n$, we may assume that that there are finitely many functions $a_1 \lt \dotsb \lt a_r \colon A \to \mathbb{R}$, definable continuous functions such that $$ \frac{\partial P}{\partial y}(\bar{x}, a_i(\bar{x}))$$ are the zeros, and the signs of the derivates are constant. We can further pass smaller constructible $A$ where $P(\bar{x}, a(\bar{x}))$ has constant signs. The point is that this is enough information to tell us how many zeros it has, and also roughly where there are. So all we need to do is to parametrize the zeros and show that it is definable. This is also easy because the graph of this function is just some part of the zero locus $P(\bar{x}, y) = 0$. In fact, we can define it as $$ (\bar{x} \in A) \wedge (a_1(\bar{x}) \lt y \lt a_2(\bar{x})) \wedge P(\bar{x}, y) = 0. $$ So we win.Proof of Lemma.
The problem is in the step when we say that the set on which the sign of $$ P(\bar{x}, a(\bar{x})) $$ is fixed is constructible. Recall that $a$ is only definable, how do we know that this is definable?
Definition 10. We say that a function $f \colon X \to \mathbb{R}$ is constructible when for constructible $T \subseteq \mathbb{R}^{p+1}$ the set $$ \lbrace (t, x) : x \in X, (t, f(x)) \in T \rbrace $$ is also constructible.
So what we need to do is to go back to the lemma, and change the condition that $\xi_\alpha$ be definable to the condition that they are constructible. At the end, this is going to be equivalent to definable, but this is something we need to do to make the argument work.