 To accommodate the new styles of variables in the model theory for many-sorted logic, we may add a domain for each style of variable. A model for a two-sorted language, for example, may consist of an ordered triple \(\langle D_1, D_2, I\rangle\) in which \(D_1\) and \(D_2\) specify the domain of quantification associated to each style of variable, and \(I\) is an interpretation function, which assigns appropriate values and extensions to each expression in the non-logical vocabulary. (Since each singular term is assigned a sort, \(I\) must be constrained to make sure singular terms of each sort denote objects in the appropriate domain.) The metatheory for many-sorted logic is closely related to the metatheory for classical quantificational logic. One may, for example, prove many-sorted versions of Compactness and the Löwenheim-Skolem Theorem. Details may be found in Enderton 2001.