The arbitrary-language graph translation (issue #12, the final transport)

The [L.IsRelational] restriction removed through the Craig Layer-3 relationalization:

• the translated root is relationalizeFormula φ ⊓ graphAxioms φ.functionsIn over graphLanguage L (relational by construction; its symbol supply may be uncountable, which is exactly why the symbol-countability wrapper came first);
• the distinguished relation survives as GraphRelation.base lt — the graph expansion and the reconstruction both preserve base relations definitionally, so chains and the rational map transport with no computation;
• chains transfer along graphExpansion (which satisfies the axioms), the wrapped relational endpoint fires, and reconstructStructure turns the graph model back into an L-model realizing φ via the capstone realize_relationalize_reconstruct.

The four public arbitrary-language endpoints of issue #12 live here: exists_model_relPreserving (Marker Theorem 4.26), wellFounded_boundedness, wellOrder_type_boundedness (Marker Corollary 4.27), and wellOrdering_undefinable.

theorem FirstOrder.Language.exists_model_relPreserving {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (h : HasWellOrderedChains φ lt) : ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (f : ℚ → M), φ.Realize M ∧ RelPreserving lt f

Marker Theorem 4.26 (arbitrary language): if φ has models with lt-chains of every countable length, then some nonempty model of φ carries a relation-preserving map f : ℚ → M — the raw positive conclusion; injectivity is a corollary under irreflexivity (RelPreserving.injective_of_irreflexive).

theorem FirstOrder.Language.wellFounded_boundedness {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (hwf : ∀ (M : Type) (x : L.Structure M), φ.Realize M → WellFounded fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]) : ∃ α < (Cardinal.aleph 1).ord, ∀ (M : Type) (x : L.Structure M), φ.Realize M → ¬∃ (w : α.ToType → M), RelChain lt α w

Boundedness, well-founded form (arbitrary language): if every model of φ interprets lt as a well-founded relation, some countable ordinal chains into no model.

theorem FirstOrder.Language.wellOrder_type_boundedness {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) (hwo : ∀ (M : Type) (x : L.Structure M), φ.Realize M → IsWellOrder M fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]) : ∃ α < (Cardinal.aleph 1).ord, ∀ (M : Type) (inst : L.Structure M) (hreal : φ.Realize M), (Ordinal.type fun (x y : M) => Structure.RelMap lt ![x, y]) < α

Boundedness, order-type form (Marker Corollary 4.27, arbitrary language): if every model of φ interprets lt as a well-order, some countable ordinal strictly bounds every model's order type.

@[reducible]

noncomputable def FirstOrder.Language.ordinalStructureFull (L : Language) (α : Ordinal.{0}) [Nonempty α.ToType] : L.Structure α.ToType

The comparison structure on an ordinal's type over an arbitrary language: every binary relation symbol is the ordinal order, other relations are empty, and functions are interpreted arbitrarily (the carrier must be nonempty — the undefinability proof uses α + 1).

Equations

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

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

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

theorem FirstOrder.Language.wellOrdering_undefinable {L : Language} (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 (arbitrary language, weak form): no sentence has as models exactly the structures whose interpreted relation is a well-order. The comparison structure on α + 1 (nonempty, so functions can be interpreted) violates the uniform order-type bound α.