Interpolation

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

def isInterpolant (φ ψ χ : Formula) : Prop

Definition of Craig interpolation for modal formulas.

Equations

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

theorem Interpolation (φ ψ : Formula) : ⊨(~φ v ψ) → ∃ (χ : Formula), isInterpolant φ ψ χ

Sorry-free interpolation theorem!