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:

1. A ⊨ C
2. C ⊨ B
3. Pred(C) ⊆ Pred(A) ∩ Pred(B)
4. 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: ∀B∃C. independent of specific B. Propositional: yes. 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.

Metatheory. Constructive proofs via cut elimination. Complexity of interpolant. Robinson joint consistency. Lyndon interpolation (polarity).

Applies to. Software verification (modular reasoning). Database theory. Ontology alignment. Knowledge compilation. Proof theory.

Limitations. Exponential interpolant size. Not all logics have it. Computational cost. Extensions subtle.

© 2026 Lingenic LLC