Malitz interpolation over an arbitrary relational language (issue #15)

Removes the countability hypothesis from malitz_interpolation_relational_countable by passing to the sublanguage generated by the two roots' own symbols — which is countable because a single Lω₁ω sentence mentions only countably many — applying the core there, and mapping the interpolant back along the inclusion.

The quantifier class survives both moves: universalSigned_restrictSymbols carries IsUniversal into the sublanguage, and universalSigned_mapLanguage carries it back out. This is the payoff of proving those as exact equivalences rather than one-way implications.

theorem FirstOrder.Language.malitz_interpolation {L : Language} [L.IsRelational] (φ ψ : L.Sentenceω) (hψ : BoundedFormulaω.IsUniversal ψ) (h : φ.Entails ψ) : ∃ (θ : L.Sentenceω), BoundedFormulaω.IsUniversal θ ∧ BoundedFormulaω.functionsIn θ ⊆ BoundedFormulaω.functionsIn φ ∩ BoundedFormulaω.functionsIn ψ ∧ BoundedFormulaω.relationsIn θ ⊆ BoundedFormulaω.relationsIn φ ∩ BoundedFormulaω.relationsIn ψ ∧ φ.Entails θ ∧ θ.Entails ψ

Malitz interpolation for L_ω₁ω (relational languages, arbitrary cardinality).

An entailment with universal consequent has a universal interpolant, whose function and relation symbols occur in both sides.

This is López–Escobar / Malitz's Theorem 4.5 in the function-free case: the interpolant may be taken in the same quantifier class as the consequent.