Selection functions for recursive functionals.
Thomas J. Grilliot · Notre Dame Journal of Formal Logic · 1969
Many of the interesting results in the study of recursive functions of finite higher types owe their existence to the way that partial recursive functions can be defined inductively by schemes.However, the profusion of notation sometimes clouds the techniques involved in working with higher types.For greater clarity and possible generalization it is natural to reinvestigate these results in the setting of inductively defined sets.In particular, the selection functions of Gandy [l, p. 14], Moschovakis [3, (I) of p. 270] and Platek [4, are basically functions that choose from a countable set of trees of computation (indexed by numbers) those trees that are the shortest.More abstractly, they are functions that choose from some objects (some of) which belong to an inductively defined set those objects that are placed in the set at the earliest stage.We prove the existence of such functions in Theorems 1 and 2. Our Theorems 3 and 4 are analogues (in the setting of inductively defined sets) of two results related to selection functions; namely, that sets r.e. in E n+2 (n >0) are not closed under type-?zquantification (proved by Moschovakis [3, Theorem 10] for the case n = 1), and that predicates r.e. in E n+2 can be characterized by a bounded existential-quantifier form (proved by Gandy [l, p. 17] for the case n = 0 and by Moschovakis [3, Theorem 9] for the case n = 1).By showing in Theorem 5 that the inductive definition of partial recursive functions fits the hypotheses of Theorems 1 through 4, we are able to obtain the known theorems related to selection functions (Theorems 6, 7 and 8) for all higher types, plus a generalization to selections from uncountable sets (Theorem 6).This generalization enables us to characterize the types of quantification under which r.e.predicates are closed (Theorem 9).We assume that the reader is familiar with the notation of the first half