 Second-order logic with general models can be thought of in terms of many sorted logic. Many sorted logic is first order logic with several different sorts of variables. Respectively, relations and functions may be between elements of different sorts. Here “sort” just means that variables of different “sorts” are kept apart by giving them different names. Otherwise the variables are just ordinary first order variables. Structures \(\mm\) of many-sorted logic have a separate domain \(M_s\) for each sort s. We may think of second-order logic as many sorted logic in which the individual variables are of a sort \(\si\), for each n the n-ary relation variables are of a sort \(\sr\), and the n-ary function variables of a sort \(s_n^{\rm fu}\). In addition there is an \(n+1\)-ary relation symbol \(\sA\) between n-tuples of individuals and n-ary relation variables indicating which n-tuples are in a relation and which are not. Finally there is an \(n+1\)-ary function symbol \(\sF\) between n-tuples of individual, individuals, and n-ary function variables indicating what value a function variable gives to each n-tuple. There are obvious first order axioms which guarantee that the many sorted logic just described faithfully mirrors second-order logic with general models.  [12]