The coded class of countable well-orders (issue #33, step 1)

wellOrderClass lt is the set of codes whose distinguished binary relation is a well-order of the carrier ℕ — the class WO as a subset of the logic space. This file freezes the class and supplies the two facts the non-Borelness argument needs about it:

• wellOrderClass_isomorphismInvariant — it is isomorphism-invariant, so López–Escobar applies to it once it is assumed Borel;
• exists_code_type_eq — every countably infinite order type is realized in it: for ω ≤ β < ω₁ some code of the class has order type exactly β. This is what contradicts the uniform bound of Marker's Corollary 4.27.

The comparison structures are the arbitrary-language ones already built for wellOrdering_undefinable (ordinalStructureFull), transported to the carrier ℕ by the generic code-transport API.

The class

def FirstOrder.Language.wellOrderClass {L : Language} [L.IsRelational] (lt : L.Relations 2) : Set L.StructureSpace

The coded well-order class: codes whose distinguished relation well-orders ℕ.

Equations

• FirstOrder.Language.wellOrderClass lt = {c : L.StructureSpace | IsWellOrder ℕ fun (x y : ℕ) => FirstOrder.Language.Structure.RelMap lt ![x, y]}

theorem FirstOrder.Language.wellOrderClass_isomorphismInvariant {L : Language} [L.IsRelational] (lt : L.Relations 2) : IsomorphismInvariant (wellOrderClass lt)

The class is isomorphism-invariant — the hypothesis López–Escobar consumes.

Every countably infinite order type occurs

theorem FirstOrder.Language.exists_code_type_eq {L : Language} [L.IsRelational] (lt : L.Relations 2) {β : Ordinal.{0}} (hinf : Ordinal.omega0 ≤ β) (hcnt : β < (Cardinal.aleph 1).ord) : ∃ (c : L.StructureSpace) (h : IsWellOrder ℕ fun (x y : ℕ) => Structure.RelMap lt ![x, y]), (Ordinal.type fun (x y : ℕ) => Structure.RelMap lt ![x, y]) = β

The order-type supply: every countably infinite ordinal is the order type of some code in the well-order class. The witness is the arbitrary-language comparison structure on β, transported to the carrier ℕ.