 As usual, to symbolize derivability of a formula from a set of formulas we write, \(\Delta \vdash \varphi\). We will write the derivability sign \(\vdash\) with a subscript when needed; namely, \(\vdash _{\MSL}\). In any of these calculi the notion of proof is effective in the sense that there is a method by which whenever a finite sequence of sequents of formulas is given, it can always be effectively determined, whether it is a proof or not. Any of these calculi is undecidable, as there is not an algorithm to check if \(\vdash \varphi\) or not. In fact, it could not be otherwise as the satisfiability problem (i.e., determining validity, or equivalently, testing for satisfiability of given formulas) for many-sorted logic is undecidable. So, we are in the same situation encountered in one-sorted first-order logic.