 The one-sorted version of interpolation was proved by William Craig in 1957a. Roger Lyndon (1959) gave a generalization of Craig’s theorem and, in 1968, Feferman extended the latter formulation to many-sorted logic (see Feferman 2008: 349). Obviously, the one-sorted version is a special case of the many-sorted one. However, many-sorted interpolation cannot be straightforwardly transferred from the one-sorted case.