On effectively discontinuous type-2 objects
Thomas J. Grilliot · Journal of Symbolic Logic · 1971
The notion of a recursive function with type-2 arguments was introduced by Kleene [4]. Soon E, the type-2 object that introduces numerical quantification, began to play a central role in the development of the theory. First, Kleene [4, XLVIII] proved that the hyperarithmetical functions are exactly the functions recursive in E. Later, Gandy [1, p. 14] proved the existence of a selection operator recursive in E (that is, some ψ(х, ), partial recursive in E, having the property that, if {х}(y, ) converges for some y, then ψ(х, ) converges and is such a y).