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.mem_wellOrderClass_iff {L : Language} [L.IsRelational] (lt : L.Relations 2) (c : L.StructureSpace) : c ∈ wellOrderClass lt ↔ IsWellOrder ℕ fun (x y : ℕ) => Structure.RelMap lt ![x, y]

def FirstOrder.Language.relIsoOfEquiv {L : Language} [L.IsRelational] (lt : L.Relations 2) {c d : L.StructureSpace} (f : L.Equiv ℕ ℕ) : (fun (x y : ℕ) => Structure.RelMap lt ![x, y]) ≃r fun (x y : ℕ) => Structure.RelMap lt ![x, y]

An L-isomorphism of decoded structures is an order isomorphism of the distinguished relations.

Equations

• FirstOrder.Language.relIsoOfEquiv lt f = { toEquiv := f.toEquiv, map_rel_iff' := ⋯ }

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.countable_toType_of_lt_omega1 {β : Ordinal.{0}} (hβ : β < (Cardinal.aleph 1).ord) : Countable β.ToType

Below ω₁ the ordinal's type is countable.

theorem FirstOrder.Language.infinite_toType_of_omega0_le {β : Ordinal.{0}} (hβ : Ordinal.omega0 ≤ β) : Infinite β.ToType

From ω on, the ordinal's type is infinite.

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