Craig interpolation for L_ω₁ω over an arbitrary language (Craig Layer 3, Unit 7a)

The full Craig interpolation theorem: no hypotheses on L. The proof is the algebraic assembly of the relationalization layer over the relational core:

1. entails_graphTranslation — the one semantic gate: r₁ ⊨ r₂ translates to Ax(F₁) ∧ r₁ʳᵉˡ ⊨ Ax(F₂) → r₂ʳᵉˡ in the graph language, by reconstructing an L-structure over F₁ ∪ F₂ from the combined graph axioms. This is the only place Unit 7 reconstructs anything.
2. The relational core craig_interpolation_relational applies in graphLanguage L (relational by construction, no countability hypothesis).
3. The interpolant's vocabulary bound rewrites through the exact occurrence identities relationsIn_graphAntecedent/relationsIn_graphConsequent and relSym_inter down to relSym L (F₁ ∩ F₂) (R₁ ∩ R₂).
4. θ := backTranslateFormula θg; the sharp bounds are Unit 6's consumer lemmas.
5. Both entailments are pure graph-expansion transport (graphExpansion_realizes_graphAxioms plus the Unit 4/Unit 6 realize bridges) — no reconstruction.

craig_pcSeparation is the arbitrary-language PC-separation wrapper (the relational craig_pcSeparation_relational stays, in the exact form issue #10 consumes).

instance FirstOrder.Language.BoundedFormulaω.instCountableFunctionsIn {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : Countable ↑φ.functionsIn

Every formula mentions only countably many function symbols — as an instance on the subtype, so graphAxioms φ.functionsIn needs no explicit countability bookkeeping.

The exact occurrence identities of the two translated sides

theorem FirstOrder.Language.relationsIn_graphAntecedent {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.and (graphAxioms (BoundedFormulaω.functionsIn r)) (relationalizeFormula r)).relationsIn = L.relSym (BoundedFormulaω.functionsIn r) (BoundedFormulaω.relationsIn r)

The graph antecedent Ax(F₁) ∧ r₁ʳᵉˡ mentions exactly the relationalization of r₁'s own symbols.

theorem FirstOrder.Language.relationsIn_graphConsequent {L : Language} (r : L.Sentenceω) : (BoundedFormulaω.imp (graphAxioms (BoundedFormulaω.functionsIn r)) (relationalizeFormula r)).relationsIn = L.relSym (BoundedFormulaω.functionsIn r) (BoundedFormulaω.relationsIn r)

The graph consequent Ax(F₂) → r₂ʳᵉˡ mentions exactly the relationalization of r₂'s own symbols.

The semantic gate: entailment translates to the graph language

theorem FirstOrder.Language.entails_graphTranslation {L : Language} (r₁ r₂ : L.Sentenceω) (h : r₁.Entails r₂) : Sentenceω.Entails (BoundedFormulaω.and (graphAxioms (BoundedFormulaω.functionsIn r₁)) (relationalizeFormula r₁)) (BoundedFormulaω.imp (graphAxioms (BoundedFormulaω.functionsIn r₂)) (relationalizeFormula r₂))

The graph translation of an entailment — the one semantic gate of the assembly, and the only place reconstruction is used: a model of Ax(F₁) ∧ r₁ʳᵉˡ that also satisfies Ax(F₂) carries the graph axioms of F₁ ∪ F₂, so it reconstructs to an L-structure in which r₁ holds; r₁ ⊨ r₂ there, and r₂ translates back.

The theorem

theorem FirstOrder.Language.craig_interpolation {L : Language} (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_ω₁ω, arbitrary language. An L_ω₁ω-entailment r₁ ⊨ r₂ over any language has an interpolant θ whose function and relation symbols each lie in the intersection of the two roots' occurrence sets, with r₁ ⊨ θ and θ ⊨ r₂.

PC-separation, arbitrary language

theorem FirstOrder.Language.craig_pcSeparation {L : Language} (ψ₁ ψ₂ : L.Sentenceω) (h : ψ₁.Entails (BoundedFormulaω.not ψ₂)) : ∃ (θ₀ : (symbSublang (BoundedFormulaω.functionsIn ψ₁ ∩ BoundedFormulaω.functionsIn ψ₂) (BoundedFormulaω.relationsIn ψ₁ ∩ BoundedFormulaω.relationsIn ψ₂)).Sentenceω), (∀ (M : Type) [inst : L.Structure M] [Nonempty M], ψ₁.Realize M → θ₀.Realize M) ∧ ∀ (M : Type) [inst : L.Structure M] [Nonempty M], ψ₂.Realize M → ¬θ₀.Realize M

Craig separation (PC-separation), arbitrary language. If ψ₁ and ψ₂ have no common model (ψ₁ ⊨ ¬ψ₂), a single shared-vocabulary sentence θ₀ separates them: it holds in the shared-vocabulary reduct of every model of ψ₁ and fails in that of every model of ψ₂.