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.

def FirstOrder.Language.dummyLang : Language

The dummy language: one function and one relation symbol at every arity.

Equations

• FirstOrder.Language.dummyLang = { Functions := fun (x : ℕ) => Unit, Relations := fun (x : ℕ) => Unit }

@[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.

noncomputable def FirstOrder.Language.uniformCollapse {L : Language} (φ : L.Sentenceω) : L →ᴸ uniformLanguage φ

The collapsing hom: φ's symbols to their sublanguage copies, every omitted function and relation to the dummy of its arity.

Equations

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

theorem FirstOrder.Language.countable_sigma_functions_uniformLanguage {L : Language} (φ : L.Sentenceω) : Countable ((n : ℕ) × (uniformLanguage φ).Functions n)

theorem FirstOrder.Language.countable_sigma_relations_uniformLanguage {L : Language} (φ : L.Sentenceω) : Countable ((n : ℕ) × (uniformLanguage φ).Relations n)

theorem FirstOrder.Language.Term.onTerm_uniformCollapse_eq {L : Language} {φ : L.Sentenceω} {α : Type} (t : L.Term α) (hF : t.functionsIn ⊆ BoundedFormulaω.functionsIn φ) : (uniformCollapse φ).onTerm t = LHom.sumInl.onTerm (restrictSymbols (BoundedFormulaω.relationsIn φ) t hF)

On terms supported in φ's function symbols, the collapse agrees with sublanguage restriction followed by sumInl.

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_uniformCollapse_eq {L : Language} {φ : L.Sentenceω} {α : Type} {n : ℕ} (ψ : L.BoundedFormulaω α n) (hF : ψ.functionsIn ⊆ functionsIn φ) (hR : ψ.relationsIn ⊆ relationsIn φ) : mapLanguage (uniformCollapse φ) ψ = mapLanguage LHom.sumInl (ψ.restrictSymbols hF hR)

The support-aware collapse identity: on formulas whose symbols lie in φ's, the collapse is sublanguage restriction followed by sumInl.

theorem FirstOrder.Language.hasArbLargeModels_mapLanguage_uniformCollapse {L : Language} {φ : L.Sentenceω} (hφarb : HasArbLargeModels φ) : HasArbLargeModels (BoundedFormulaω.mapLanguage (uniformCollapse φ) φ)

Source-side semantics: a model of φ becomes a model of the collapsed sentence — sublanguage symbols genuinely, dummy functions constantly (the model is nonempty by the size request), dummy relations as False. So the collapsed sentence inherits arbitrarily large models.

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.