Well-Orderings

Origin. Tarski's first paper on the subject is from 1921 ("Przyczynek do aksjomatyki zbioru dobrze uporządkowanego"). Mostowski and Tarski announced the elementary classification in 1949 ("Arithmetical classes and types of well-ordered systems"); the full analysis waited nearly thirty years and appeared as Doner, Mostowski, and Tarski, "The elementary theory of well-ordering — a metamathematical study" (Logic Colloquium '77, 1978, pp. 1–54). Doner and Tarski, "An extended arithmetic of ordinal numbers" (Fund. Math. 65, 1969), handles the ordinal operations. Jeřábek (2024) gives a short proof of both the axiomatization and the decidability.

Models. Ordinals, as a first-order theory of order alone. The theory is decidable, and the reason is that first-order logic sees almost nothing of a well-ordering: every ordinal is elementarily equivalent to one below ω^ω·2, so the entire class of well-orderings has countably many elementary types and each is decided. This is DLO's sibling with the order type inverted — dense and endpoint-free there, well-founded here, decidable in both cases, and for the same reason: the language cannot code.

Formalism.

Language: < (binary), =.

Axioms (Doner–Mostowski–Tarski; presentation after Jeřábek): LO the axioms of strict linear order (irreflexive, transitive, total) TI transfinite induction schema, for every formula φ (parameters allowed): ∀x (∀y (y < x → φ(y)) → φ(x)) → ∀x φ(x)

Th(WO) = LO + TI. That is the whole axiomatization: well-foundedness is not first-order expressible, and transfinite induction over definable classes is exactly the first-order shadow of it — the same relation induction bears to ℕ in Peano arithmetic, and the same schema.

Decidability (Doner–Mostowski–Tarski 1978): Th(WO) is decidable. Their proof is syntactic quantifier elimination, which takes work, since properties of Cantor normal forms turn out to be definable in the theory and must be handled. Alternative route: the MSO theory of countable linear orders interprets into S2S, decidable by Rabin's tree theorem — correct, and disproportionate. Läuchli–Leonard's technique for the theory of linear orders gives the short proof.

The elementary classification (Mostowski–Tarski): Write α = ω^ω·α₁ + α₂ with α₂ < ω^ω. α ≡ β ⟺ α₂ = β₂ and (α₁ = β₁ = 0 or α₁, β₁ > 0) So the ordinals below ω^ω·2 form a complete and irredundant set of representatives of the elementary equivalence classes of well-orderings. Everything above ω^ω·2 is elementarily equivalent to something below it: first-order logic can count up to ω^ω and then sees only "some" or "none".

Ordinal arithmetic: Th(⟨On, +⟩) — ordinal addition — is decidable (Ehrenfeucht; Maurin's Ehrenfeucht-game proof, 1997). Choffrut handles addition with left translation by ω. Ordinal multiplication: Bès (2002) gives the definability and decidability results; the fragments of ⟨ω^(ω^λ); ×⟩ have a mixed decidable/undecidable landscape. Doner–Tarski (1969) axiomatize the extended arithmetic of ordinals.

Comparison, within this subdivision: DLO — dense, no endpoints; ℵ₀-categorical; QE in the bare language; o-minimal; unstable. WO — well-founded; not categorical in any cardinal; QE after expansion; ℵ₀ many complete extensions; unstable. Both decidable, neither interprets Q. The pair brackets the order-theoretic case: the two order types mathematics uses most, both settled, both settled by the same absence — no pairing, no coding.

Symbols.

Metatheory. Th(WO) is axiomatized by transfinite induction and decidable, and the classification explains both: only ω^ω·2 many elementary types, each decided, so first-order logic's view of the ordinals terminates at ω^ω. That is a sharp statement of how weak the order language is, and it is worth setting against what the collection does elsewhere with ordinals — Ordinal Analysis assigns ε₀ to PA and Γ₀ to predicative analysis, and every distinction it draws is invisible to Th(WO), which cannot tell ε₀ from ω^ω·2. The ordinals of proof theory are ordinal notations, carrying the recursive structure the elementary theory discards; the entry is here so that the objects being notated have their own theory stated, and so that the gap between them is visible. Well-foundedness itself is not first-order — TI is its definable shadow, exactly as PA's induction schema is the shadow of second-order induction, and non-standard models follow for the same reason.

Applies to. Ordinal arithmetic and its decision procedures. Model theory of linear orders, as the well-founded half alongside DLO. Automata on ordinals and transfinite automata recursions (Büchi 1965), where the decidability results come from the automata side. Termination proofs and ordinal-based ranking functions in verification, where the question is what an ordinal assignment can express. Proof theory, as the contrast case: the elementary theory of the ordinals is decidable, and nothing in ordinal analysis follows from it.

Limitations. First-order logic sees ordinals only up to ω^ω, so the theory is decidable by being blind — it cannot express well-foundedness, cannot distinguish ε₀ from a countable ordinal below ω^ω·2, and contributes nothing to the proof theory that uses ordinals. The QE proof is technical out of proportion to the statement, since Cantor normal forms are definable and must be managed; the short proofs came fifty years after the result. Non-standard models exist, and "the theory of well-orderings" has models that are not well-orderings — the class WO is not first-order axiomatizable, only its theory is. Ordinal multiplication's landscape is only partly mapped.

© 2026 Lingenic LLC