The Theorems of A. Robinson, Craig and Beth

Abstract

In this chapter we shall prove two important new results about first-order predicate logic: Craig’s interpolation lemma (1957) and Beth’ s definability theorem (1953). The interpolation lemma states that, for any expressions α, γ such that α ╞ γ, there is an “interpolating” expression β such that any variable which occurs free in β occurs free in both α and γ and such that α ╞ β and β ╞ γ. The definability theorem states that an “implicit definition” within the framework of the language of ordinary predicate logic can always be changed into an “explicit definition”. More precisely, the following holds (in this introduction we shall restrict ourselves to the case of a one-place predicate variable P): Let α be an expression which “implicity defines” P in the sense that, in every interpretation I which satisfies a, the predicate I(P) is uniquely determined by the I-images of the other variables. (This can also be formulated as follows: If P’ is a one-place predicate variable which does not occur in α and which is different from P, and if a’ if obtained from α by replacing Pby P” everywhere in α, then α ⋀ α’ ╞ ⋀x(Px ↔ P’x).)