 The first thing we do is to set a many-sorted language \(\MSL^{\PML}\) containing: unary relation symbols for each atomic proposition, \(P\in \Atom\), a binary relation symbol \(S\) to represent the accessibility relation, a membership sign, and equality for individuals and sets. \(\MSL^{\PML}\) contains individual variables as well as variables for sets. The translation is standard (as in  section 3.2):  we express in the target logic \(\MSL^{\PML}\) the semantical interpretation of the formulas being  translated.[21]  In particular,