Published online by Cambridge University Press: 12 March 2014
One of the most fundamental results of higher-type recursion theory was first proved by Thomas Grilliot [3]. He showed that the functional embodying number quantification, 2E, is computable from a type-2 object F if and only if F has an effective discontinuity. For the background to this work we recommend Normann's book [9] or his summary [10], and for an example of its many applications Normann-Wainer [11].
The purpose of §1 of this paper is to give an effective proof of the “only if” part of this result: i.e. a construction of a discontinuity of F from the information 2E = {e}F. This contrasts with Grilliot's argument which is topological and nonconstructive, and shows that “Grilliot's trick” for computing 2E from a discontinuity of F is essentially the only method.
We then apply the method to two more general situations in which it gives new results. In §2 we treat type-3 objects in which 3E is computable (assuming AC and CH), and obtain a strengthening of the result of Hartley [5, §5]. In §3 we consider the superjump and characterise it as the least among a class of functionals with a particular sort of family of discontinuities.