Interpolation (Sections 2.3 and 7)

def Interpolant (φ ψ θ : Formula) : Prop

An interpolant θ for φ and ψ only uses the vocabulary in both, is implied by φ and implies ψ.

Equations

• Interpolant φ ψ θ = (θ.voc ⊆ φ.voc ∩ ψ.voc ∧ tautology (~φ⋀(~θ)) ∧ tautology (~θ⋀(~ψ)))

theorem interpolation {φ ψ : Formula} : tautology (~φ⋀(~ψ)) → ∃ (θ : Formula), Interpolant φ ψ θ