DLO is the theory of dense linear orders (without endpoints). A model of DLO is a linearly ordered set (M, < ) satisfying the following additional conditions:
∀x∀y : x < y → ∃z : x < z < y
∀x∃y : x < y
∀x∃y : y < x.
For example, (ℚ, < ) and (ℝ, < ) are models, but (ℤ, < ) is not, and neither is the extended real line, or the interval [0, 1].
DLO is o-minimal, countably categorical, and NIP, but not uncountably categorical, stable, or simple. It has quantifier elimination in the language with the ordering. It has elimination of imaginaries in the weak sense that every element of Meq is interdefinable with an element of the home sort (right?), but there are quotients that cannot be eliminated. In particular, after naming two elements, DLO has elimination of imaginaries in every sense of the word.
DLO is the model companion of totally ordered sets, and can be seen as a Fraïsse limit of finite total orderings. ::: ::: :::