 The idea for Craig’s 1957 proof of the Interpolation Theorem rests on the completeness theorem for one-sorted first-order logic. The reason is that interpolation “lies” somehow in the intersection of proof theory (as it follows from some metatheorems about the calculus) and model theory (because of its applications). Henkin showed that the other way round also holds: completeness can be immediately obtained from a extended  version[31]  of Craig-Lyndon’s theorem.