Non-Borelness of the countable well-order class (issue #33)

The descriptive-set-theoretic payoff of Marker's boundedness theorem: the class WO of countable well-orders is not Borel as a subset of the logic space.

theorem wellOrderClass_not_measurableSet (lt : L.Relations 2) : ¬ MeasurableSet (wellOrderClass lt)

Were it Borel, López–Escobar (#10) would give a sentence φ with ModelsOf φ = WO — but only over coded structures, whose carrier is ℕ. The bridge from there to arbitrary models is the fragment-elementary substructure machinery (#13), applied to φ ⊓ infiniteAxiom so that finite models cannot escape:

• exists_countable_defect_seed — a structure whose distinguished relation is not a well-order carries a countable nonempty seed of witnesses (a trichotomy or transitivity failure, or the range of an infinite descending sequence) whose presence forces the same failure in every subset containing it;
• isWellOrder_of_realize — hence every model of φ ⊓ infiniteAxiom is well-ordered: seed a countable fragment-elementary substructure with the defect, transport it to the carrier ℕ, and the resulting code would be a member of ModelsOf φ = WO that is not a well-order.

Marker's Corollary 4.27 then bounds the order types of all models of φ ⊓ infiniteAxiom by a single countable ordinal, which exists_code_type_eq contradicts.

The defect seed

theorem FirstOrder.Language.exists_countable_defect_seed {M : Type} {r : M → M → Prop} (h : ¬IsWellOrder M r) : ∃ (X : Set M), X.Countable ∧ X.Nonempty ∧ ∀ (N : Set M), X ⊆ N → ¬IsWellOrder ↑N fun (x y : ↑N) => r ↑x ↑y

A structure whose relation fails to be a well-order carries a countable nonempty seed of witnesses: every subset containing the seed inherits the failure. In this Mathlib a well-order is trichotomy plus well-foundedness (transitivity is derived), so there are exactly two cases: a two-element trichotomy failure, and the range of an infinite descending sequence.

The bridge: coded definability forces every model to be well-ordered

theorem FirstOrder.Language.isWellOrder_of_realize {L : Language} [L.IsRelational] (lt : L.Relations 2) {φ : L.Sentenceω} (hφ : ModelsOf φ = wellOrderClass lt) (M : Type) [instM : L.Structure M] (hM : Sentenceω.Realize (BoundedFormulaω.and φ L.infiniteAxiom) M) : IsWellOrder M fun (x y : M) => Structure.RelMap lt ![x, y]

The bridge (#13's role in this argument): if a sentence defines the well-order class on codes, then every model of that sentence conjoined with the infiniteness axiom interprets the distinguished relation as a well-order. A defect would survive into a countable fragment-elementary substructure seeded with its witnesses, and that substructure — infinite by the added conjunct — transports to a code of ModelsOf φ that is not a well-order.

The endpoint

theorem FirstOrder.Language.wellOrderClass_not_measurableSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (lt : L.Relations 2) : ¬MeasurableSet (wellOrderClass lt)

The countable well-order class is not Borel (issue #33): no Borel set of codes consists exactly of the well-ordered ones.