Functionals defined by recursion.
Luis Elpidio Sanchis · Notre Dame Journal of Formal Logic · 1967
Recursive functionals of finite type have been studied by several authors in recent years.The class of functionals that can be defined by primitive recursion of finite type is certainly more constructive than other more inclusive classes, as the general recursive functionals studied by Kleene.Moreover functionals defined by recursion are sufficient for the interpretation of formal systems of number theory in the manner described by Godel in [3].In this paper we study a formalization of the class of functionals which are closed under explicit definition and recursion.Combinators, first studied in combinatory logic, play a central role in this formalization.They are used first to obtain closure under explicit definition and second to formalize definitions by recursion.For this purpose new operators of a special kind must be introduced.But they behave in a manner quite similar to ordinary combinators, and we intend to use the same name for both kinds of operators.The system is constructed as an equation calculus in the usual way in combinatory logic.It is proved that the rules are complete in the sense that whenever an equation with variables is derivable, the corresponding equation (without variables) of higher type is also derivable without using variables.This generalizes the well known principle of extensionality in combinatory logic. 1 We also analyse a kind of reduction of terms by means of replacements.It is shown that every constant term of the type of natural numbers can be reduced in that way to a numeral.This can be generalized for constant terms of higher type and the result is applied to prove the consistency of the equation calculus.Results of the same sort, were obtained by Tait in [11].We have used several ideas and methods that are current in combinatory logic, but the paper is self contained.In the work of Curry it has been customary to avoid the assignment of a definite type to the combinators.We shall depart from this procedure by requiring every entity of the system to have a definite type.We need in this way to assume an infinite number of combinators.Grzegorczyk has studied in [4] a very similar formalism.The standpoint there is mainly semantical.We plan to discuss in a forthcoming paper the possibility of formalizing the arguments of [4] in our