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. Five 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.

Symbol	Unicode	Name	Meaning
¬	U+00AC	Negation	Irreflexivity: ¬(x < x)
×	U+00D7	Multiplication sign	Lexicographic product of orders
κ	U+03BA	Kappa	An uncountable cardinal, in κ-categoricity
ℚ	U+211A	Rationals	The unique countable model
ℝ	U+211D	Reals	An uncountable model, not distinguishable from ℚ
ℤ	U+2124	Integers	Model of the discrete variant, not of DLO
ℵ	U+2135	Alef	Cardinal notation, as in ℵ₀-categoricity
→	U+2192	Rightwards arrow	Material implication in the axioms
∀	U+2200	Universal quantifier	Every axiom is universally closed
∃	U+2203	Existential quantifier	Density and endpoint-freeness
∖	U+2216	Set minus	Removing a point, as in ℝ ∖ {0}
∧	U+2227	Conjunction	Joins order constraints
∨	U+2228	Disjunction	Trichotomy
≺	U+227A	Precedes	The order, when < is taken
≅	U+2245	Isomorphism	What Cantor's argument produces
≡	U+2261	Elementary equivalence	All models, to each other
⋀	U+22C0	N-ary conjunction	Finite conjunction in the elimination step
⟨	U+27E8	Angle bracket, left	Opens a structure, as in ⟨ℚ, <⟩
⟩	U+27E9	Angle bracket, right	Closes a structure
<	—	Less than	The single non-logical symbol of the language
=	—	Equality	The only other atomic relation
DLO	—	Dense linear order	Without endpoints
ℵ₀	—	Aleph-null	Countable cardinality; DLO is ℵ₀-categorical
2^ℵ₀	—	Cardinality of the continuum	Size of the non-isomorphic uncountable models
Aut	—	Automorphism group	Aut(ℚ, <), highly transitive and homogeneous

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.