Namely, the set of validities of \(\XL\) is recursively enumerable. Therefore, \(\XL\) is complete in an abstract sense. Remark: So, we learn that a calculus for \(\XL\) is a natural demand, but we also learn that in MSL we can simulate such a calculus and then we could use a theorem prover for MSL. 5 Level Two: the Main Theorem When the \(\XL\) logic under scrutiny has a concept of logical consequence, we may try to prove the Main theorem; that is, that consequence in \(\XL\) (\(\Pi \models _