Craig’s interpolation theorem a theorem for firstorder logic: if a sentence y of first-order logic entails a sentence q there is an ‘interpolant,’ a sentence F in the vocabulary common to q and y that entails q and is entailed by y. Originally, William Craig proved his theorem in 1957 as a lemma, to give a simpler proof of Beth’s definability theorem, but the result now stands on its own. In abstract model theory, logics for which an interpolation theorem holds are said to have the Craig interpolation property. Craig’s interpolation theorem shows that first-order logic is closed under implicit definability, so that the concepts embodied in first-order logic are all given explicitly.
In the philosophy of science literature ‘Craig’s theorem’ usually refers to another result of Craig’s: that any recursively enumerable set of sentences of first-order logic can be axiomatized. This has been used to argue that theoretical terms are in principle eliminable from empirical theories. Assuming that an empirical theory can be axiomatized in first-order logic, i.e., that there is a recursive set of first-order sentences from which all theorems of the theory can be proven, it follows that the set of consequences of the axioms in an ‘observational’ sublanguage is a recursively enumerable set. Thus, by Craig’s theorem, there is a set of axioms for this subtheory, the Craig-reduct, that contains only observation terms. Interestingly, the Craig-reduct theory may be semantically weaker, in the sense that it may have models that cannot be extended to a model of the full theory. The existence of such a model would prove that the theoretical terms cannot all be defined on the basis of the observational vocabulary only, a result related to Beth’s definability theorem.
See also BETH’S DEFINABILITY THEOREM, PROOF THEORY. Z.G.S.