Recursive Functionals and Quantifiers of Finite Types Revisited, V (Q3978437)

This paper is the last in a series of five where the author gives a new foundation for recursion in higher type functionals. The general idea of the program is described in the review of Part IV [Recursion Theory, Proc. AMS-ASL Summer Inst., Ithaka/N.Y. 1982, Proc. Symp. Pure Math. 42, 119-138 (1985; Zbl 0608.03015)]. It is essential to read a considerable part of paper 4 before reading this paper. This paper consists of \(\S\S\)14 through 19. In \(\S\)14 the author develops his notion of computation further, explaining how the computations are run. In \(\S\)15 he proves some structural results about the computations and in \(\S\)16 he shows that the computations are monotone with respect to the input. In \(\S\)17 he shows that the computable functionals will be in the hierarchy of monotone, partial functionals with oracles. In \(\S\)18 he shows that equivalent algorithms, or j-expressions, can replace each other. Finally in \(\S\)19 he compares ordinary typed elements with typed elements with oracles. Through his five papers the author has made a remarkable effort to create a new foundation for higher type recursion theory. The idea of a computation being organised through a unique well founded tree of subcomputations does not work for computations relative to partial, monotone functionals. Equipping the functionals with oracles makes the construction more natural. The hard point is to ensure that the choice of oracle is inessential. This is taken care of by Kleene, and the foundation is sound.