 The general plan is as follows: The signature of the logic being studied (call it \(\XL\)) is transformed into a many-sorted signature, the expressions of the logic \(\XL\) are translated into \(\MSL^{\XL}\) (a many-sorted language suited for \(\XL\)) and the structures of the logic \(\XL\) are converted into many-sorted structures. Thus, we need to define a recursive function \(\Trans\) to do the translation and a direct conversion of structures, \(\Conv_{1}.\)