 Next question to ask is whether or not \(\mathfrak{S}^{\ast}\) can be replaced by the models of a set \(\Delta\) of many-sorted formulas. Thus, the key to both definitions, \(\Trans\) and \(\Conv_{1}\), is to simplify the proof of the semantic equivalence, and in this respect the relevance of the results obtained strongly depends on the possibility of axiomatizing \(\mathfrak{S}^{\ast}\). In case you get such a recursive set of formulas of \(\MSL^{\XL}\), say \(\Delta\), (or at least such that \(\mathfrak{S}^{\ast}\subseteq \Mod(\Delta )\)) we should prove that validity in \(\XL\) is equivalent to consequence from \(\Delta\) in \(\MSL^{\XL}\).