 However, the move to a many-sorted language is largely a matter of convenience. Many-sorted quantification may be analyzed in terms of restricted one-sorted quantification. For each many-sorted language with \(n\) styles of variable, we may introduce a one-sorted language, which comes with a one-place predicate, \(S_i\), for each sort in the many-sorted language. We may set out to translate each formula of the many-sorted language into a formula of the one-sorted language: we translate each identity in terms of a single identity predicate; a quantification on a variable of sort \(i\), \(\forall x^i A\), is replaced with a formula of the form \(\forall x(S_i x \rightarrow A)\). We may, in addition, turn each model for the many-sorted language \(\langle D_1, \ldots, D_n, I \rangle\) into a model for the resulting one-sorted language \(\langle \bigcup_{n} D_n, I^\ast \rangle\) in which we take the domain to consist in the union of the domains associated to each original sort. The interpretation function, \(I^\ast\) will coincide with \(I\) when it comes to predicates and individual constants. However, \(I^\ast\) will generally have to extend the interpretation of a functional symbol, \(f^n_i\), by \(I\), in one way or another. Finally, \(I^\ast\) will interpret the identity predicate as usual.