 However, other theorems about many-sorted logic are not straightforwardly obtained from their one-sorted versions. In particular, interpolation in MSL requires its own proof (see  section 6.2).  The concept of interpretability plays an important role for a comparison between one-sorted and many-sorted theories (see  section 6.3  and Hook 1985). Unfortunately, interpretablity between many-sorted theories is not obtained from their one-sorted counterparts. Concerning the comparison, deductions in a many-sorted proof system are usually shorter than the derivations we get in a one-sorted calculus, that is one of the reasons why many-sorted logic is so frequently used in Computer Science (Meinke &amp; Tucker 1993).