 A related use of many-sorted logic is to provide a kind of translation from second-order logic into a first-order logic. In this case instead of having second-order quantification over sets (or properties), one stays with a first-order language which is supplemented with a predicate true of all and only sets (or properties), a distinct style of variables for those entities, and with a two-place relation of either membership or instantiation.