 In case we wanted to prove that modal calculi for K and S4 (see the entry on  modal logic)  are complete by using the completeness of MSL, Deductive Correspondence between the modal logic concerned and its many-sorted counterpart have to be proved. Proving deductive correspondence from propositional modal logic to many-sorted logic is easy