Lyndon's interpolation theorem
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.
Reading path
To understand this page from the ground up, read these 2 pages in order. The foundations come first. The path takes the proof Proof of Lyndon's interpolation theorem.
Show the path as a graph
- no evidence level
Further reading
- Wikipedia, page 2056790, revision 1321826961, Craig interpolation, section Lyndon's interpolation theorem. adopted
About this page
| Tag | BRDT1BT7WW |
|---|---|
| URI | m2://BRDT1BT7WW |
| Kind | statement, theorem |
| Writing | W0 stub |
| Status | This copy of the site has no build data. Run m2 status BRDT1BT7WW. |
| Changed | 4 November 2026 |
Markdown · JSON · Edit on GitHub
What this page needs for W1
- edge uses out: each definition that the statement needs (0 of 1)
The writing levels say how complete the text of a page is. They do not measure its truth.