 Let \(L\) be a second-order language with a set \(\OperSym\) of operation symbols. If we compare expressions in SOL with expressions in a many-sorted logic, we realize that \(X^{n}x_{1}\ldots x_{n}\) is not a formula of many-sorted logic since it is only a string of variables. What we do is to introduce a new many-sorted language, \(\MSL^{\SOL}\), where we retain all the symbols in \(\OperSym\) but the signature is now enlarged with new membership relation symbols, \(\epsilon _{n}\), whose interpretations are going to be a kind of membership relations. The many-sorted signature \(\Sigma ^{\SOL}\) includes a set \(\Sorts\) whose elements are the types in the SOL structure; namely, 1, and \(\langle\underbrace{ 1,\ldots ,1}_n ,0\rangle\) for all \(n\geq  1\).[17]