 The semantics of many-sorted logic is rather similar to that of classical first-order logic, because it follows Tarski’s truth definition to introduce the concept of truth in a structure (see Tarski 1933 and Tarski &amp; Vaught 1956; for historical clarifications, see Hodges 1986 and the entry on  Tarski’s truth definitions).  In our case, the object language is many-sorted logic and the metalanguage is set theory. Set theory is the commonly used metalanguage, where relation symbols are interpreted as relations defined over universes (sets) of mathematical structures.