Logical interpolation

Every logical consequence passes through an intermediary making use only of the resources in common between the assumption and the consequence.

Suppose that we are faced with a logical entailment from premise φ to conclusion ψ:

\( φ ⊨ ψ\)

Perhaps the assertions do not involve altogether exactly the same propositional vocabularly. Perhaps the premise φ makes statements involving propositional atoms not appearing in the conclusion, and the conclusion ψ involves propositional atoms not appearing in the premise. One might wonder whether those extra propositional atoms are actually relevant for the entailment—might we be able somehow to eliminate them or separate them out?

Indeed, the method of interpolation exactly fulfills this expectation. Specifically, an interpolant for a validity φ ⊨ ψ is a sentence λ standing logically between the premise and the conclusion in the sense that both φ ⊨ λ and λ ⊨ ψ hold, but furthermore such that every propositional atom appearing in λ is mentioned both in φ and in ψ. Thus, we will have eliminated the irrelevant atoms—the logical force of the original entailment passes through the interpolant, like a baseball thrown at the window.

The baseball interpolates between player and window

The interpolant makes use only of the propositional atoms common to the premise and conclusion.

For a simple example, consider the following entailment: