Craig interpolation for L_ω₁ω, countable relational core (issue #8, Layer 1)

The internal countable joint-language Craig theorem. Its conclusion is already a base-L interpolant — L[[ℕ]] occurs only inside the proof, at the abstraction boundary given by the three constant-expansion transport equalities below.

craig_interpolation_relational_countable :
  Sentenceω.Entails r₁ r₂ →
    ∃ θ, θ.functionsIn ⊆ r₁.functionsIn ∩ r₂.functionsIn ∧
         θ.relationsIn ⊆ r₁.relationsIn ∩ r₂.relationsIn ∧
         Sentenceω.Entails r₁ θ ∧ Sentenceω.Entails θ r₂

No coverage or side-bound hypotheses are needed: the side vocabularies are specialized to the roots' exact occurrence sets, and the paired family (PairedInsepFamily.lean) maintains coordinatewise side membership field-by-field, so the audit's global GenU ⊆ Sent₁ ∪ Sent₂ coverage invariant — and with it the coverage hypothesis — is unnecessary (an audit correction).

The root argument

Assume no interpolant. Then the mapped root pair ({r₁'}, {r₂'.not}) is inseparable at empty support: an empty-support separator would strip (base_interpolant_of_empty_support_separator) to a base interpolant θ₀ with r₁ ⊨ θ₀ and {r₂.not} ⊨ θ₀.not, and the latter is θ₀ ⊨ r₂ by semantic contraposition — contradiction. Feeding the inseparable root pair to exists_paired_model_neg gives one model with M ⊨ r₁ and ¬ M ⊨ r₂; its base reduct contradicts r₁ ⊨ r₂.

The three constant-expansion transport equalities (the base-L ↔ L[[ℕ]] boundary)

theorem FirstOrder.Language.baseFunctionsIn_mapLanguage_withConstants {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r).baseFunctionsIn = BoundedFormulaω.functionsIn r

Base functions of a constant-expansion image are the sentence's own functions.

theorem FirstOrder.Language.baseRelationsIn_mapLanguage_withConstants {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r).baseRelationsIn = BoundedFormulaω.relationsIn r

Base relations of a constant-expansion image are the sentence's own relations.

theorem FirstOrder.Language.sentenceJConsts_mapLanguage_withConstants {L : Language} (r : L.Sentenceω) : sentenceJConsts (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) r) = ∅

A constant-expansion image carries no constants: its constant support is empty.

The semantic contraposition / singleton bridge

theorem FirstOrder.Language.entails_singleton_of_neg_entails_neg {L : Language} {r₂ θ : L.Sentenceω} (hE : {BoundedFormulaω.not r₂}.Entails (BoundedFormulaω.not θ)) : {θ}.Entails r₂

Semantic contraposition (singleton form): {r₂.not} ⊨ θ.not is {θ} ⊨ r₂.

The countable relational Craig theorem

theorem FirstOrder.Language.craig_interpolation_relational_countable {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (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_ω₁ω — countable relational core. Over a relational language with countably many relation symbols, an L_ω₁ω-entailment r₁ ⊨ r₂ has a base-L interpolant whose function/relation symbols lie in the intersection of the roots' occurrence sets.