Dense Linear Orders (DLO)

Origin. Cantor (1895) proved that any two countable dense linear orders without endpoints are isomorphic — the back-and-forth argument, and the first categoricity theorem in mathematics. Langford (1927) gave the quantifier elimination and the decision procedure, making DLO the first nontrivial theory shown complete and decidable, two years before Presburger's arithmetic.

Models. The rationals, up to elementary equivalence and — in the countable case — up to isomorphism. Four axioms describe an order that is linear, dense, and has no first or last element, and Cantor's argument shows nothing else is needed: ℚ is the unique countable model, and every model is elementarily equivalent to it. ℝ is a model too, and DLO cannot tell it apart from ℚ, which is the standard first demonstration that first-order logic does not see completeness of an order.

Formalism.

Language: < (binary), =.

Axioms: D1. ∀x ¬(x < x) (irreflexive) D2. ∀x∀y∀z (x < y ∧ y < z → x < z) (transitive) D3. ∀x∀y (x < y ∨ x = y ∨ y < x) (total) D4. ∀x∀y (x < y → ∃z (x < z ∧ z < y)) (dense) D5. ∀x ∃y (y < x) ∧ ∀x ∃y (x < y) (no endpoints)

Finitely axiomatized. Five axioms, no schema.

Quantifier elimination: immediate, in the language itself — no expansion needed, unlike Presburger's. Every formula is equivalent to a Boolean combination of atomic formulas xᵢ < xⱼ and xᵢ = xⱼ. The elimination step: ∃y (⋀ᵢ aᵢ < y ∧ ⋀ⱼ y < bⱼ) is equivalent to ⋀ᵢⱼ aᵢ < bⱼ, by density; the endpoint-free axioms handle the degenerate cases.

Consequences of QE: Complete — QE plus a decidable quantifier-free theory over the empty signature. Decidable — the elimination is effective. Model complete; in fact it has elimination of quantifiers, which is stronger. The definable subsets of any model are exactly the finite unions of points and open intervals with endpoints in the model. DLO is o-minimal, and it is the simplest o-minimal theory.

Categoricity: ℵ₀-categorical (Cantor's back-and-forth): the unique countable model is ⟨ℚ, <⟩. Not κ-categorical for any uncountable κ — ⟨ℝ, <⟩ and ⟨ℝ ∖ {0}, <⟩ and ℚ × ℝ (lexicographic) are non-isomorphic models of size 2^ℵ₀. By the Ryll-Nardzewski theorem, ℵ₀-categoricity is equivalent to finitely many n-types for each n; DLO's types are the orderings of the variables, of which there are finitely many.

Fraïssé limit: ⟨ℚ, <⟩ is the Fraïssé limit of the class of finite linear orders. It is the unique countable homogeneous model, and Aut(ℚ, <) is one of the standard examples in the model theory of automorphism groups.

Variants: DLO with endpoints, with one endpoint — each complete, decidable, and mutually non-elementarily-equivalent to DLO. The theory of discrete linear orders without endpoints is complete and decidable too, with ⟨ℤ, <⟩ as a model, but is not ℵ₀-categorical.

Symbols.

Metatheory. DLO is where every technique in model theory is first shown to work: back-and-forth for categoricity, quantifier elimination for completeness and decidability, Ehrenfeucht–Fraïssé games for elementary equivalence, Fraïssé construction for ℚ as a limit, Ryll-Nardzewski for the type-counting characterization, o-minimality in its simplest instance. It is unstable — the order property is definable by x < y, and the order property is the definition of instability — so it also marks the boundary of stability theory from the outside. Five axioms with no schema and no coding: DLO does not interpret Q, has no pairing, and is decidable for the same reason Presburger is, that the signature cannot express sequences.

Applies to. Model theory pedagogy and practice, as the standard first example of every technique. O-minimality, as the base case. Temporal logic and interval reasoning, where dense linear time is the intended frame — the entries in Modal/Temporal and Applications/Spatial that assume density assume this theory. Automorphism group theory and topological dynamics, via Aut(ℚ, <). Constraint solving over ordered domains.

Limitations. The theory sees nothing but order: no arithmetic, no metric, no completeness of the order — Dedekind completeness is not first-order expressible, and DLO cannot distinguish ℚ from ℝ, which is either the point or the defect depending on what is wanted. Not uncountably categorical, so Morley's theorem contributes nothing here. Its simplicity is what makes it useful and what makes it uninteresting on its own: every question about DLO is answered, and has been since 1927.

© 2026 Lingenic LLC