 Definition 4.1 \({T}\) has a many-sorted language in that each terms is assigned a type. Type (symbols) are generated from 0 by the rule: If \(\sigma\) and \(\tau\) are types then so is \(\sigma\to\tau\). Intuitively the ground type 0 is the type of natural numbers. If \(\sigma\) and \(\tau\) are types that are already understood then \(\sigma\to\tau\) is a type whose objects are considered to be functions from objects of type \(\sigma\) to objects of type \(\tau\). In addition to variables \(x^{\tau},y^{\tau},z^{\tau},\ldots\) for each type \(\tau\), the language of \({T}\) has special constants 0, \(\rsuc\), \(\rK_{\sigma,\tau}\), \(\rS_{\rho,\sigma,\tau}\), and \(\rR_{\sigma}\) for all types \(\rho,\sigma,\tau\). The meaning of these constants is explained by their defining equations. \(\rK_{\sigma,\tau}\) and \(\rS_{\rho,\sigma,\tau}\) are familiar from combinatory logic which was introduced by Schönfinkel in 1924 and became more widely known through Curry’s work (1930). 0 plays the role of the first natural number while \(\rsuc\) embodies the successor function on objects of type 0. The constants \(\rR_{\sigma}\), called recursors, provide the main vehicle for defining functionals by recursion on \(\bbN\). Term formation starts with constants and variables, and if s and t are terms of type \(\sigma\to\tau\) and \(\sigma\), respectively, then \(s(t)\) is a term of type \(\tau\). To increase readability we shall write \(t(r,s)\) instead of \((t(r))(s)\) and \(t(r,s,q)\) instead of \((t(r,s))(q)\) etc. Also \(\rsuc(t)\) will be shortened to \(t'\). The defining axioms for the constants are the  following:[17]