Lyndon interpolation, ambient relational theorem (issue #14, Unit 5, commit 3)

The public relational endpoint, with no global countability hypothesis: pass to the sublanguage generated by the two roots' (countably many) symbols, apply the countable core there, and map the interpolant back along the inclusion — transporting the two signed occurrence bounds by the exact image law relationsInSigned_mapLanguage.

lyndon_interpolation_relational [L.IsRelational] (r₁ r₂ : L.Sentenceω) :
  Sentenceω.Entails r₁ r₂ →
    ∃ θ, θ.functionsIn ⊆ r₁.functionsIn ∩ r₂.functionsIn ∧
         θ.positiveRelationsIn ⊆ r₁.positiveRelationsIn ∩ r₂.positiveRelationsIn ∧
         θ.negativeRelationsIn ⊆ r₁.negativeRelationsIn ∩ r₂.negativeRelationsIn ∧
         Sentenceω.Entails r₁ θ ∧ Sentenceω.Entails θ r₂

This is the relation-polarity / logical-equality form of López–Escobar 1965, Theorem 4.1: its clause (.4) in full, with clause (.3)'s equality-occurrence condition deliberately not claimed (equality is logical here, and unconstrained in the interpolant).

lyndon_interpolant_is_craig recovers the unsigned Craig bound from the two signed ones through relationsIn = positive ∪ negative; it is a consumer lemma, so Craig interpolation is visibly recoverable without duplicating the existing craig_interpolation_relational.

theorem FirstOrder.Language.lyndon_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ω.positiveRelationsIn θ ⊆ BoundedFormulaω.positiveRelationsIn r₁ ∩ BoundedFormulaω.positiveRelationsIn r₂ ∧ BoundedFormulaω.negativeRelationsIn θ ⊆ BoundedFormulaω.negativeRelationsIn r₁ ∩ BoundedFormulaω.negativeRelationsIn r₂ ∧ r₁.Entails θ ∧ θ.Entails r₂

Lyndon 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 function symbols lie in the intersection of the roots' function occurrences, whose positively occurring relation symbols lie in the intersection of the roots' positive occurrences, and whose negatively occurring ones lie in the intersection of the roots' negative occurrences.

The relation-polarity / logical-equality form of López–Escobar 1965, Theorem 4.1 — clause (.4) in full; clause (.3)'s equality-occurrence condition is not claimed.

theorem FirstOrder.Language.lyndon_interpolant_is_craig {L : Language} {θ r₁ r₂ : L.Sentenceω} (hp : BoundedFormulaω.positiveRelationsIn θ ⊆ BoundedFormulaω.positiveRelationsIn r₁ ∩ BoundedFormulaω.positiveRelationsIn r₂) (hn : BoundedFormulaω.negativeRelationsIn θ ⊆ BoundedFormulaω.negativeRelationsIn r₁ ∩ BoundedFormulaω.negativeRelationsIn r₂) : BoundedFormulaω.relationsIn θ ⊆ BoundedFormulaω.relationsIn r₁ ∩ BoundedFormulaω.relationsIn r₂

Craig from Lyndon, at the occurrence level. The unsigned shared-vocabulary bound follows from the two signed bounds through relationsIn = positive ∪ negative. Stated as a consumer lemma so that the recovery of Craig interpolation is explicit, without duplicating the existing craig_interpolation_relational.