ABSTRACT
Our goal now is to prove the Craig lemma, a kind of “Occam Razor” principle for logic. The idea here is that when an implication ψ ⇒ ϕ is a tautology, then this phenomenon means that there is a constraint on the variables that occur both in ψ and ϕ. This constraint, ϑ must be entailed by the constraint expressed by ψ and in itself must entail ϕ. This limitation on the variables that are mentioned in ϑ is the reason why we mentioned “Occam Razor.” It turns out that, actually, the requirements can be more stringent, and we can find even better intermediate constraints (they are called interpolants), with additional limitations on the polarity of variables involved.
The Craig lemma, in its simplest form, states that whenever ψ ⇒ ϕ is a tautology, then there exists an interpolant, a formula ϑ, involving only the variables occurring both in ψ and in ϕ, such that both ψ ⇒ ϑ and ϑ⇒ ϕ are tautologies.
