 For more on the reduction of second-order logic to many-sorted logic, we refer to Manzano (1996). For example, the proof theory of second-order logic can be understood via the translation to many sorted logic. For more on the proof theory of second-order logic, see Buss (1998). There is a translation of many sorted logic further to single sorted first order logic due essentially to Herbrand (1930), see also Wang (1952) and Schmidt (1951). This can be used to obtain many of the basic properties of first order logic first for many sorted logic and then further for second-order logic with general models.