 Apart from its reduction to one-sorted logic, many-sorted first-order logic can be extended. Sort logic is a many-sorted second-order logic in which it is allowed to quantify over new sorts, “looking outside” the structure where the formula is being interpreted. Then, besides adding sorts to a second-order logic, we may include a new logical symbol \(\widetilde{\exists }\) to quantify over new sorts.