nLab Craig interpolation theorem

Idea

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).

Related Concepts

• definability
• first-order logic
• Beth definability theorem
• Löwenheim-Skolem theorem
• Robinson consistency theorem
• conceptual completeness
• abstract model theory
• descent theory

References

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:

• C. C. Chang, H. J. Keisler, Model Theory , North-Holland Amsterdam 1973.

A textbook account that covers the classical as well as the intuitionistic case is in:

• John Bell, Moshé Machover, A Course in Mathematical Logic , North-Holland Amsterdam 1977.

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:

• John Bell, A. B. Slomson, Models and Ultraproducts: An Introduction , North-Holland Amsterdam 1969.

The bible on interpolation in non-classical logic is:

• Dov Gabbay, Larisa Maksimova, Interpolation and Definability - Modal and Intuitionistic Logics , Oxford UP 2005.

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)