Lyndon interpolation, arbitrary language (issue #14, Unit 7)

The hypothesis-free endpoint: no relationality assumption, no countability assumption.

lyndon_interpolation (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₂

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), now over an arbitrary language.

The assembly is Craig's, reused verbatim wherever polarity is irrelevant:

• entails_graphTranslation — the one semantic gate, unchanged;
• the relational Lyndon theorem applied inside graphLanguage L;
• the function-symbol bound comes from the unsigned graph bound, obtained from the two signed bounds by lyndon_interpolant_is_craig composed with Craig's exact occurrence identities and relSym_inter — exactly the route craig_interpolation takes;
• the signed base-relation bounds come from Unit 6: the signed back-translation identity plus the two preimage root corollaries (preimage_baseRelSym_graphAnd/Imp);
• both entailments are Craig's graph-expansion arguments, unchanged.

theorem FirstOrder.Language.lyndon_interpolation {L : Language} (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_ω₁ω, arbitrary language. An entailment r₁ ⊨ r₂ over any language has an interpolant whose function symbols lie in the intersection of the roots' function occurrences, whose positive relation occurrences lie in the intersection of the roots' positive occurrences, and whose negative 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, with clause (.3)'s equality-occurrence condition deliberately not claimed.

theorem FirstOrder.Language.craig_of_lyndon_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 from Lyndon, arbitrary language. The unsigned shared-vocabulary bound follows from the two signed ones; stated so the recovery is explicit without duplicating craig_interpolation.