Undefinability of well-ordering (issue #12, step 6 layer 3)

The packaging layer, deliberately distinguishing two inequivalent statements:

• the strong form is layer 2's uniform order-type bound (wellOrder_type_boundedness_relational): every sentence all of whose models are well-ordered has its order types bounded by a single countable ordinal;
• the weak form proved here (wellOrdering_undefinable_relational): no sentence has as models exactly the structures whose interpreted relation is a well-order — the ordinal α produced by the bound is itself a well-order of type α, so it would be a model violating its own bound.

The countable-coded/Borel form of undefinability (¬ MeasurableSet of the well-order class, issue #33) is not this statement: it additionally needs López–Escobar and the countable fragment-elementary-substructure bridge, and stays in #33.

The witness structure interprets every binary relation symbol as the ordinal order and every other arity as empty — this avoids deciding equality against the distinguished symbol lt, which a general language does not support.

def FirstOrder.Language.ordRel (α : Ordinal.{0}) (n : ℕ) : (Fin n → α.ToType) → Prop

The all-arities relation family on an ordinal's type: binary positions get the ordinal order, every other arity is empty.

Equations

• FirstOrder.Language.ordRel α 2 v = (v 0 < v 1)
• FirstOrder.Language.ordRel α x✝¹ x✝ = False

@[reducible]

def FirstOrder.Language.ordinalStructure (L : Language) [L.IsRelational] (α : Ordinal.{0}) : L.Structure α.ToType

The comparison structure on an ordinal's type over a relational language: every binary relation symbol is the ordinal order, everything else is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.ordinalStructure_relMap (L : Language) [L.IsRelational] (α : Ordinal.{0}) (lt : L.Relations 2) (x y : α.ToType) : Structure.RelMap lt ![x, y] ↔ x < y

Any binary relation symbol of the comparison structure is the ordinal order.

theorem FirstOrder.Language.ordinalStructure_isWellOrder (L : Language) [L.IsRelational] (α : Ordinal.{0}) (lt : L.Relations 2) : IsWellOrder α.ToType fun (x y : α.ToType) => Structure.RelMap lt ![x, y]

The comparison structure interprets any binary relation symbol as a well-order.

theorem FirstOrder.Language.wellOrdering_undefinable_relational {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (lt : L.Relations 2) : ¬∃ (φ : L.Sentenceω), ∀ (M : Type) (x : L.Structure M), φ.Realize M ↔ IsWellOrder M fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]

Undefinability of well-ordering (weak form, relational/countable): no sentence has as models exactly the structures whose interpreted relation is a well-order. From the uniform order-type bound: the bounding ordinal α, as a comparison structure, would be a model of order type α < α.