 The previous theorem allows us to infer the following three semantic theorems for MSL from the corresponding one-sorted results: Compactness theorem, Enumerability theorem and Löwenheim-Skolem theorem (see Enderton 1972: 281). But we have obtained them already as we have proven completeness for MSL  (section 2.3).  Obviously, from the many-sorted theorems we get the one-sorted version for free.