The uniform collapsing language (issue #11 unit 7b)

The arbitrary-language wrapper for the small-model theorem cannot expand a countable-language model back to L with arbitrary interpretations — smallness does not ascend through arbitrary expansions. The clean fix is a COLLAPSING LANGUAGE HOM: uniformLanguage φ is the two-sorted generated sublanguage of φ plus one dummy function and one dummy relation at every arity, and uniformCollapse φ : L →ᴸ uniformLanguage φ sends φ's symbols to their genuine sublanguage copies and every omitted symbol to the dummy. The final full-language structure is then LITERALLY a reduct along uniformCollapse φ, so semantics for every full-language formula are supplied generically (realize_mapLanguage) and smallness descends by Lomega1omegaSmall.of_expansion. This file provides:

• the language, the hom, and countability of the target's symbols;
• the support-aware syntactic identity mapLanguage_uniformCollapse_eq — on formulas whose symbols lie in φ's, the collapse agrees with sublanguage restriction followed by sumInl;
• the source-side semantics hasArbLargeModels_mapLanguage_uniformCollapse: models of φ (requested at size ≥ max μ ℵ₀, so nonempty and the dummies are interpretable) become models of the collapsed sentence.

@[reducible]

def FirstOrder.Language.uniformLanguage {L : Language} (φ : L.Sentenceω) : Language

The uniform countable target: φ's generated sublanguage plus the dummies.

Equations

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

theorem FirstOrder.Language.exists_small_model_of_hasArbLargeModels {L : Language} {φ : L.Sentenceω} (hφarb : HasArbLargeModels φ) {κ : Cardinal.{0}} (hκ : Cardinal.aleph0 ≤ κ) : ∃ (N : Type) (x : L.Structure N), φ.Realize N ∧ Cardinal.mk N = κ ∧ Lomega1omegaSmall N

The small-model theorem (Marker, Theorem 11.2), over an ARBITRARY language: a sentence with arbitrarily large models has, at every infinite κ, a model of size exactly κ realizing only countably many complete L_{ω₁ω}-types. The final structure is literally the reduct of the countable-language small model along uniformCollapse φ, so satisfaction is generic (realize_mapLanguage) and smallness descends (Lomega1omegaSmall.of_expansion); the carrier and hence its cardinality are unchanged.