Prove theory of DLO has quantifier elimination

[eionblanc]

As a critical step in implementing o-minimality, we need to show that the theory of dense linear orders without endpoints (DLOWE or just DLO) admits quantifier elimination (QE). That is, we will show that any formula in our model (Q; <) is equivalent to a quantifier-free formula.

[eionblanc]

O-minimality of (Q; <) will then essentially be a corollary---think about what the sets defined by quantifier-free formulas are in this language; in Q, they are either points (via =) or intervals (via <), so the definable sets are boolean combinations of these.

[eionblanc]

Here are some helpful links.

• This is a quick primer on what quantifier elimination is and does. The nice part is that we can reduce to the case of showing QE for formulas with just one existential quantifier and a conjunction of atomic formulas. This reduction might be tricky in Lean, though.
• This has the proof that we need (Theorem 4.3.4); it's surprisingly simple but still might be difficult to understand on your first read.