 Currently, the proliferation of logical systems used in mathematics, computer science, philosophy, and linguistics makes the relationships between and their possible translations into one another a pressing issue. We saw above that many-sorted logic is a natural logic for reasoning about more than one sort of objects. In this section, we will present it as a unifying framework in which we may situate most of the many logics available to us. The general plan of translations into MSL is described with some details. Three possible levels of translations are settled and, at each level, when successfully reached, one completeness result is gained: abstract completeness at the first level, strong completeness at the third. Therefore, when a logic is translated into many-sorted logic we only need a unique deductive calculus, the many-sorted one, as well as an efficient theorem prover. In cases like basic propositional modal logic, where formulas could be translated into a decidable fragment of first-order logic with only two variables, the translation mechanism implies decidability for the modal logic. Moreover, some metaproperties of many-sorted logic can be transferred to the logic being translated.