---
tag: BRDT1BT7WW
kind: statement
role: theorem
name: Lyndon's interpolation theorem
sources:
  - wikipedia: en:2056790@r1321826961
    locator: Craig interpolation, section Lyndon's interpolation theorem
    note: adopted
    mention: wikipedia://en/2056790#BUCI
    sections: [Statement]
inventory: [CWW1NZDZSW]
---

## Statement

Suppose that *S* and *T* are two first-order theories. As notation, let *S* ∪ *T* denote the smallest theory including both *S* and *T*; the signature of *S* ∪ *T* is the smallest one containing the signatures of *S* and *T*. Also let *S* ∩ *T* be the intersection of the languages of the two theories; the signature of *S* ∩ *T* is the intersection of the signatures of the two languages.

Lyndon's theorem says that if *S* ∪ *T* is unsatisfiable, then there is an interpolating sentence ρ in the language of *S* ∩ *T* that is true in all models of *S* and false in all models of *T*. Moreover, ρ has the stronger property that every relation symbol that has a positive occurrence in ρ has a positive occurrence in some formula of *S* and a negative occurrence in some formula of *T*, and every relation symbol with a negative occurrence in ρ has a negative occurrence in some formula of *S* and a positive occurrence in some formula of *T*.