 In  section 5.2,  a variety of modal systems are treated (including S4, whose accessibility relation is reflexive and transitive) and several metatheorems are proved for them, by using the MSL reservoir. The translation is defined into a many-sorted first-order logic with a second-order flavor, as the many-sorted structures used in that section contain the relevant categories of mathematical sets (and relations) definable in the modal logic being translated.