Craig interpolation for L_ω₁ω, relational core without a global countability hypothesis (Layer 2)

Layer 1 (craig_interpolation_relational_countable) needs the whole language to have countably many relation symbols. This layer removes that hypothesis: an individual L_ω₁ω sentence mentions only countably many symbols (relationsIn_countable), so the two roots r₁, r₂ live inside the sublanguage symbSublang F R generated by their (countable) combined symbol sets, which is countable-relational. We restrict both roots into that sublanguage, transport the entailment (entails_restrictSymbols_singleton), apply Layer 1 there, and map the interpolant back along symbSublangIncl — the reduct transport keeps the two entailments and the occurrence bounds intact.

craig_interpolation_relational [L.IsRelational] :
  Sentenceω.Entails r₁ r₂ →
    ∃ θ, θ.functionsIn ⊆ r₁.functionsIn ∩ r₂.functionsIn ∧
         θ.relationsIn ⊆ r₁.relationsIn ∩ r₂.relationsIn ∧
         Sentenceω.Entails r₁ θ ∧ Sentenceω.Entails θ r₂

instance FirstOrder.Language.symbSublang_isRelational {L : Language} [h : L.IsRelational] (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : (symbSublang F R).IsRelational

A symbol-generated sublanguage of a relational language is relational: the function subtypes are carved out of already-empty function sorts.

Mapping a sublanguage interpolant back to L: entailment and occurrence transport

These four transports are generic in the sublanguage inclusion — nothing about them is specific to Craig — so they are exported for the Lyndon refinement (issue #14, Unit 5), which needs the same entailment and function-occurrence transports alongside its own signed relation transport.

theorem FirstOrder.Language.entails_mapLanguage_restrictSymbols_left {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (r : L.Sentenceω) (hF : BoundedFormulaω.functionsIn r ⊆ F) (hR : BoundedFormulaω.relationsIn r ⊆ R) (θ' : (symbSublang F R).Sentenceω) (hE : Sentenceω.Entails (BoundedFormulaω.restrictSymbols r hF hR) θ') : r.Entails (BoundedFormulaω.mapLanguage (symbSublangIncl F R) θ')

Left entailment transport: a sublanguage entailment r₁.restrictSymbols ⊨ θ' lifts, along the inclusion, to r₁ ⊨ θ'.mapLanguage incl in L (via the sublanguage reduct of an L-model).

theorem FirstOrder.Language.entails_mapLanguage_restrictSymbols_right {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (r : L.Sentenceω) (hF : BoundedFormulaω.functionsIn r ⊆ F) (hR : BoundedFormulaω.relationsIn r ⊆ R) (θ' : (symbSublang F R).Sentenceω) (hE : θ'.Entails (BoundedFormulaω.restrictSymbols r hF hR)) : Sentenceω.Entails (BoundedFormulaω.mapLanguage (symbSublangIncl F R) θ') r

Right entailment transport: a sublanguage entailment θ' ⊨ r₂.restrictSymbols lifts to θ'.mapLanguage incl ⊨ r₂ in L.

theorem FirstOrder.Language.functionsIn_mapLanguage_incl_subset {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (r : L.Sentenceω) (hF : BoundedFormulaω.functionsIn r ⊆ F) (hR : BoundedFormulaω.relationsIn r ⊆ R) (θ' : (symbSublang F R).Sentenceω) (hsub : BoundedFormulaω.functionsIn θ' ⊆ (BoundedFormulaω.restrictSymbols r hF hR).functionsIn) : (BoundedFormulaω.mapLanguage (symbSublangIncl F R) θ').functionsIn ⊆ BoundedFormulaω.functionsIn r

Function-occurrence transport: the mapped interpolant's functions stay within r's functions, given the sublanguage bound against the restriction.

theorem FirstOrder.Language.relationsIn_mapLanguage_incl_subset {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (r : L.Sentenceω) (hF : BoundedFormulaω.functionsIn r ⊆ F) (hR : BoundedFormulaω.relationsIn r ⊆ R) (θ' : (symbSublang F R).Sentenceω) (hsub : BoundedFormulaω.relationsIn θ' ⊆ (BoundedFormulaω.restrictSymbols r hF hR).relationsIn) : (BoundedFormulaω.mapLanguage (symbSublangIncl F R) θ').relationsIn ⊆ BoundedFormulaω.relationsIn r

Relation-occurrence transport (companion of the above for relation symbols).

The relational Craig theorem (no global countability hypothesis)

theorem FirstOrder.Language.craig_interpolation_relational {L : Language} [L.IsRelational] (r₁ r₂ : L.Sentenceω) (h : r₁.Entails r₂) : ∃ (θ : L.Sentenceω), BoundedFormulaω.functionsIn θ ⊆ BoundedFormulaω.functionsIn r₁ ∩ BoundedFormulaω.functionsIn r₂ ∧ BoundedFormulaω.relationsIn θ ⊆ BoundedFormulaω.relationsIn r₁ ∩ BoundedFormulaω.relationsIn r₂ ∧ r₁.Entails θ ∧ θ.Entails r₂

Craig interpolation for L_ω₁ω — relational, no global countability hypothesis. Over a purely relational language (of arbitrarily many symbols), an L_ω₁ω-entailment r₁ ⊨ r₂ has a base-L interpolant whose symbols lie in the intersection of the roots' occurrence sets.