Interpolation

Abstract

Interpolation is one of the most important topics of logic and model theory. Below is a very simple example. Consider the following semantic deduction in PL (propositional logic):

$$ p_1 \wedge q \vDash p_2 \vee q $$

where p₁, p₂, q are propositional symbols (i.e., relation symbols of zero arity). The simplest justification for this deduction is by factoring it as

$$ p_1 \wedge q \vDash q \vDash p_2 \vee q $$

which meets the intuition that p₁ is not involved in establishing the truth of p₂ ∨ q. In general, the so-called ‘Craig interpolation’ (abbreviated CI) property can be formulated as follows: if ρ₁ ⊨ ρ₂ for two sentences, then there exists a sentence ρ, called the interpolant of ρ₁ and ρ₂, that uses logical symbols that appear both in ρ₁ and ρ₂ and such that ρ₁ ⊨ ρ ⊨ ρ₂. An equivalent expression of the above property assumes ρ₁ ⊨ ρ₂ in the union signature Σ₁ ∪ Σ₂, and asks for ρ to be in the intersection signature Σ₁ ∩ Σ₂, where Σ _i is the signature of ρ _i .