 The theorem cannot be established for many-sorted logic by simply translating \(\varphi\) and \(\psi\) to the corresponding formulas of a one-sorted language. It is easy to see that the logical form of a constructed interpolant for \(\vdash \Trans(\varphi )\rightarrow \Trans(\psi )\) is not necessarily equivalent to a translation of a many-sorted formula. This is why we said that this result could not be straightforwardly transferred from the one-sorted case (see Otto 2000 for more details).