Equivalence of some definitions of recursion in a higher type object
F. Lowenthal · Journal of Symbolic Logic · 1976
In [4] Kleene gave a definition of recursive functionals of finite type. Later Sacks [5] and Harrington [2] gave definitions of recursion in normal functionals of finite type. These definitions, that Sacks and Harrington assumed equivalent as far as normal objects are concerned, are nevertheless very different: Kleene's definition is given in terms of an inductive definition; Sacks uses simultaneously a hierarchy (the SσF's) and induction on the ordinals and on the type; Harrington's universe does not use the induction on the type but uses a hierarchy as Shoenfield [6]. In this paper we prove in detail that, as was expected, the three definitions are equivalent.