 Sometimes in applications of first order logic, i.e., when we are dealing at length with a specific class of interpretations the domain divides into intuitively disparate kinds of objects, e.g., people and numbers. In the usual formulation, one has predicates, e.g., Px and Nx which are true of those kinds of things respectively, and so one translates the English sentence “All numbers are odd” as \((\forall x)(Nx \rightarrow Ox)\) and “Some person is tall” as \((\exists x)(Px \mathbin{\&amp;} Tx)\). In a many-sorted logic distinct variables are used for the different kinds of objects, perhaps m, n,… for numbers and p, q,… for people. In this language combinations of variables with predicates are sometimes restricted so that Nm and Tp are well-formed but Np and Tn are not. If one does not make this restriction then the notation is exactly equivalent to standard first-order logic. A many-sorted language is expressively equivalent to a single sorted one which has additional predicates for the various sorts of things (cf. Quine 1966).