Craig Interpolation
Origin. William Craig (1957). If A ⊨ B, there exists interpolant C. C uses only shared vocabulary. Fundamental theorem linking syntax and semantics. Applications across logic.
Models. A ⊨ B implies ∃C. A ⊨ C and C ⊨ B. Language(C) ⊆ Language(A) ∩ Language(B). Constructive in many systems.
Formalism.
Craig's theorem (first-order): If A ⊨ B and A, B share at least one predicate, then ∃C such that:
- A ⊨ C
- C ⊨ B
- Pred(C) ⊆ Pred(A) ∩ Pred(B)
- Free(C) ⊆ Free(A) ∩ Free(B)
Propositional form: If A → B is valid, interpolant C exists with Var(C) ⊆ Var(A) ∩ Var(B).
Constructive interpolation: Proof-theoretic: extract C from cut-free proof of A → B. Sequent calculus: midsequent theorem.
Uniform interpolation: ∃C ∀B — the quantifier order is the whole content. Fix A and a sublanguage L; a uniform interpolant is a single C ∈ L with A ⊨ C such that C ⊨ B for every B ∈ L with A ⊨ B. C depends on A and L alone. Written ∀B ∃C it says nothing beyond ordinary Craig interpolation, which already produces an interpolant for each B separately. The strength is in choosing C before B is known. Propositional: yes — substitute ⊤ and ⊥ for the non-shared variables and disjoin. Intuitionistic propositional: yes (Pitts). First-order: no in general.
Failures: Some modal logics lack interpolation. Some many-sorted logics fail. Second-order logic: restricted interpolation.
Beth definability (corollary): Implicit definability ⇔ explicit definability. If Σ uniquely determines relation R, R is Σ-definable.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| ⊨ | U+22A8 | Entails | Semantic consequence |
| ∩ | U+2229 | Intersection | Shared vocabulary |
| ⊆ | U+2286 | Subset | Vocabulary containment condition on the interpolant |
| ∃ | U+2203 | Existential quantifier | "There is an interpolant" |
| ∀ | U+2200 | Universal quantifier | Quantifier order in uniform interpolation |
| → | U+2192 | Rightwards arrow | Material implication A → B |
| ⇔ | U+21D4 | If and only if | Beth: implicit iff explicit definability |
| ⊤ | U+22A4 | Verum | Substituted for non-shared variables |
| ⊥ | U+22A5 | Falsum | Substituted for non-shared variables |
| Σ | U+03A3 | Sigma | A theory that defines a relation implicitly |
| Pred | — | Predicates | Relation symbols of a formula |
| Free | — | Free variables | Free variables of a formula |
| Var | — | Variables | Propositional variables of a formula |
Metatheory. Craig, "Three uses of the Herbrand–Gentzen theorem in relating model theory and proof theory" (JSL, 1957), proved interpolation for first-order logic by cut elimination, so the interpolant is extracted from the proof rather than merely shown to exist. Lyndon (1959) strengthened it to respect polarity, which yields the classical preservation theorems; Robinson's joint consistency theorem (1956) is equivalent to Craig's, and Beth's definability theorem (1953) follows from it. Interpolation is exceptional rather than typical among non-classical logics: Maksimova (1977) proved that exactly eight superintuitionistic propositional logics have Craig interpolation, and her later classification found only finitely many normal extensions of S4 with the property. Uniform interpolation cuts finer still — Pitts (1992) established it for intuitionistic propositional logic and Ghilardi for K, while Ghilardi and Zawadowski (1995) showed S4 has Craig interpolation but not uniform interpolation, and first-order logic has none. On the complexity side, Krajíček and Pudlák established feasible interpolation for resolution — an interpolant circuit of size polynomial in the refutation — and Mundici showed that polynomial-size interpolants for all propositional pairs would put NP ∩ coNP inside P/poly.
Applies to. Software verification (modular reasoning). Database theory. Ontology alignment. Knowledge compilation. Proof theory.
Limitations. Craig's theorem is an existence statement with a side condition: if A and B share no non-logical symbol, the only available interpolants are ⊤ and ⊥, so the theorem then degenerates into "A is unsatisfiable or B is valid". Interpolants can be unavoidably large — by Mundici's argument, polynomial-size interpolants for all propositional entailments would collapse NP ∩ coNP into P/poly — and feasible interpolation is known to fail for strong proof systems such as Extended Frege under standard cryptographic assumptions, so proof-theoretic extraction does not scale. The property is not inherited: adding a modality, a cardinality quantifier, or second-order quantification generally destroys it, and Maksimova's classifications show that the logics retaining it form a finite and rather thin list. Uniform interpolation, which is what modular reasoning actually wants, fails for first-order logic and for S4. Finally, the preservation theorems that Craig and Lyndon interpolation deliver are theorems about arbitrary structures: Łoś–Tarski fails over finite structures, so the corollaries do not transfer to finite model theory, and only the homomorphism preservation theorem was recovered there, by Rossman in 2008.
© 2026 Lingenic LLC