In many-sorted logic we have several "sorts" of variables, just as in vector spaces we have scalars and vectors, or as in geometry we have points and lines, or as in second-order logic we have individuals and subsets. Although many-sorted logic can be translated into one-sorted logic, it is often more natural to take the many-sorted approach, and sometimes the many-sorted version of a fundamental theorem is more powerful than the single-sorted version. This is the case, for example, with the Craig Interpolation Theorem which we prove in the many-sorted version. We will discuss various applications of many-sorted logic, among others applications of the many-sorted interpolation theorem. Time permitting, I will talk about a "symbiosis" between set theory and model theory, based on many-sorted logic.
