Thinness of the coded well-orders in the pure one-strict-order language

In kbLanguage, whose only symbol is the binary kbRelSym.lt, the coded well-order class is thin for isomorphism (kbLanguage.wellOrderClass_isThinOn): no perfect set of pairwise non-isomorphic coded well-orders. The route is the existing analytic boundedness theorem, not any counting of types:

1. a continuous Cantor antichain in the class has compact, hence analytic, range inside the class;
2. analytic_wellOrder_type_boundedness bounds its order types below one countable ordinal β;
3. in the pure language, equal order types give order isomorphisms (Ordinal.type_eq), which are structure isomorphisms (equivOfRelIso, the converse of relIsoOfEquiv);
4. the antichain would therefore inject Cantor space into the countable set of ordinals below β (countable_Iio_of_lt_omega1), which is impossible.

Why the language is restricted

For an arbitrary relational L, wellOrderClass lt constrains only the distinguished relation. With one extra unary predicate U, keep the usual order on ℕ and let U vary over Cantor space: the order is rigid, so distinct colourings are non-isomorphic, and the codes depend continuously on the colouring, giving a continuous Cantor antichain inside wellOrderClass lt. So thinness of wellOrderClass lt is false in general, and the theorem below is stated for the pure language only; the general definition of wellOrderClass is unchanged.

Nothing here uses the sentence-spectrum or fragment-spectrum characterizations, and no determining cover appears: this consumer validates the boundedness handoff, not the counting machinery.

@[reducible, inline]

abbrev FirstOrder.Language.kbLanguage.codeRel (c : kbLanguage.StructureSpace) (x y : ℕ) : Prop

The distinguished relation of a kbLanguage code, as a binary relation on ℕ.

Equations

• FirstOrder.Language.kbLanguage.codeRel c x y = FirstOrder.Language.Structure.RelMap FirstOrder.Language.kbRelSym.lt ![x, y]

def FirstOrder.Language.kbLanguage.equivOfRelIso {c d : kbLanguage.StructureSpace} (e : codeRel c ≃r codeRel d) : kbLanguage.Equiv ℕ ℕ

In the pure language, an order isomorphism of the distinguished relations is a structure isomorphism: the converse of relIsoOfEquiv.

Equations

• FirstOrder.Language.kbLanguage.equivOfRelIso e = { toEquiv := e.toEquiv, map_fun' := ⋯, map_rel' := ⋯ }

theorem FirstOrder.Language.kbLanguage.not_hasCantorAntichainOn_wellOrderClass : ¬HasCantorAntichainOn kbLanguage.structureIsoSetoid (wellOrderClass kbRelSym.lt)

Coded well-orders in the pure language carry no Cantor isomorphism antichain.

theorem FirstOrder.Language.kbLanguage.wellOrderClass_isThinOn : IsThinOn kbLanguage.structureIsoSetoid (wellOrderClass kbRelSym.lt)

Thinness of the coded well-orders in the pure one-strict-order language.