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