indiscernible sequence?
Morley sequence?
Ramsey theorem?
Erdos-Rado theorem?
Ehrenfeucht-Fraïssé games (back-and-forth games)
The Craig interpolation theorem is a basic result in the model theory of first-order logic.
First proved by W. Craig for classical predicate calculus in 1957, it has been extended to intuitionistic logic by K. Schütte in 1962. Andrew M. Pitts and Michael Makkai have proved variants in categorical logic e.g. for pretoposes. Diaconescu proved an abstract variant in institution-independent model theory (cf. Augier-Barbier(2007), Diaconescu(2008)).
Craig interpolation theorem. Let $\varphi_1,\varphi_2$ be first-order sentences over the vocabularies $\mathcal{L}_1,\mathcal{L}_2$ such that $\varphi_1\models\varphi_2$. Then there is a sentence $\theta$ over the common vocabulary $\mathcal{L}_1\cap\mathcal{L}_2$, the interpolant, such that $\varphi_1\models\theta$ and $\theta\models\varphi_2$.
An important corollary is the Beth definability theorem.
The theorem plays an important role in abstract model theory where the question whether the Craig interpolation property can take over the role of the Löwenheim-Skolem theorem in Lindström's theorems, has been called ‘one of the main open problems of the field’ by Väänänen (2008, p.404).
The original source is
William Craig, Linear Reasoning. A new form of the Herbrand-Gentzen theorem , JSL 22 (1957) pp.250-268.
William Craig, Three uses of the Herbrand-Gentzen Theorem in relating model theory and proof theory, JSL 22 (1957) pp.269-285.
For an account in a standard reference see:
A textbook account that covers the classical as well as the intuitionistic case is in:
For a proof that uses Keisler’s ultrapower theorem (Roughly: $\mathcal{A}\equiv\mathcal{B}$ iff $\mathcal{A}^I/F\cong\mathcal{B}^I/G$ for some ultrafilters $F,G$ on I) see:
The bible on interpolation in non-classical logic is:
The following provides background on proofs of Craig’s theorem and categorical logic in a gentle way:
Michael Makkai, On Gabbay’s Proof of the Craig Interpolation Theorem for Intuitionistic Predicate Logic, Notre Dame J. Form. Logic 36 no. 3 (1995) pp.364-381. (pdf)
M. Aiguier, F. Barbier, An institution-independent Proof of the Beth Definability Theorem , Studia Logica 85 no. 3 (2007) pp.333-359. (pdf)
Razvan Diaconescu, Institution-indepent Model Theory , Birkhäuser Basel 2008.
Andrew M. Pitts, Amalgamation and Interpolation in the Category of Heyting algebras , JPAA 29 (1983) pp.155-165.
Andrew M. Pitts, An Application of Open Maps to Categorical Logic , JPAA 29 (1983) pp.313-326.
Jouko Väänänen, The Craig Interpolation Theorem and abstract model theory , Synthese 164:401 (2008) (freely available online)
Last revised on June 8, 2017 at 05:57:23. See the history of this page for a list of all contributions to it.