Interpolation

We use everything we have proven so far to show that GL has interpolation!

def Lean4GlCoalgebras.isInterpolant (φ ψ χ : Formula) : Prop

Definition of Craig interpolation.

Equations

• Lean4GlCoalgebras.isInterpolant φ ψ χ = (χ.vocab ⊆ φ.vocab ∩ ψ.vocab ∧ ⊨(~φ v χ) ∧ ⊨(~χ v ψ))

theorem Lean4GlCoalgebras.interpolation (φ ψ : Formula) : ⊨(~φ v ψ) → ∃ (χ : Formula), isInterpolant φ ψ χ

Sorry-free interpolation theorem!