 In consequence, the terms of many-sorted logic are defined recursively as follows: Each variable or individual constant of sort \(s_{i}\) is a term of the same sort \(s_{i}\). If \(f\in \OperSym\) is such that \(\Rank(f)=\langle i_{1},\ldots,i_{m},i_{0}\rangle\) with \(i_{0}\not=0\) and \(\tau _{1},\ldots,\tau _{m}\) are terms of sorts \(i_{1},\ldots,i_{m}\), then \(f\ \tau _{1}\ldots\tau _{m}\) is a term of sort \(i_{0}\).