Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-26T21:39:40.994Z Has data issue: false hasContentIssue false
  • English
  • Français

Selection in abstract recursion theory

Published online by Cambridge University Press:  12 March 2014

L. A. Harrington  and
D. B. Macqueen
L. A. Harrington
Affiliation:
Suny at Buffalo, Amherst, New York 14226
D. B. Macqueen
Affiliation:
Air Force Institute of Technology, Wright-Patterson AFB, Ohio 45433
Get access Rights & Permissions [Opens in a new window]

Extract

In [1] Gandy established the following selection theorem for recursion in type-2 objects.

Theorem. Let F be a normal type-2 object. Then it is possible to select (uniformly and effectively in F) an integer from each nonempty set of integers semirecursive in F .

Notice that this really asserts that the predicates semirecursive in F are closed under existential quantification over type-0. Moschovakis [6] has essentially proven this theorem for F of arbitrary type.

In [2] Grilliot stated a powerful generalization of Gandy's result, namely:

Grilliot's Selection Theorem. Let F be a normal type-(n + 2) object (n an arbitrary integer). Then it is possible to select (uniformly and effectively in F) a nonempty recursive in F subset of each nonempty semirecursive in F set oftype-(n − 1) objects.

Notice again that this actually says that predicates semirecursive in F are closed under quantification over type-(n − 1) objects.

Despite the similarity of these two results, Gandy and Grilliot proposed rather different methods of proof. Furthermore, the proof that Grilliot presented in [2] contains an error which cannot easily be corrected. (We will comment on the nature of this error at the end of §1.) Fortunately, however, Grilliot's theorem is valid. We will present a proof of Grilliot's selection theorem which is a direct generalization of the proof of Gandy's theorem given in [6]. In fact, we will prove a general result (the theorem stated in §2) which subsumes both Gandy's and Grilliot's results.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 41 , Issue 1 , March 1976 , pp. 153 - 158
Copyright
Copyright © Association for Symbolic Logic 1976

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Gandy, R. O., General recursive functionate of finite type and hierarchies of functions, paper given at the symposium on mathematical logic held at the University of Clermont Ferrand, 06 1962.Google Scholar
[2] Grilliot, T. J., Selection functions for recursive functionate, Notre Dante Journal of Formal Logic, vol. 10 (1969), pp. 225–234.Google Scholar
[3] Grilliot, T. J., Inductive definitions and computability, Transactions of the American Mathematical Society, vol. 158 (1971), pp. 309–317.CrossRefGoogle Scholar
[4] Kleene, S. C., Recursive functionate and quantifiers of finite type. I, II, Transactions of the American Mathematical Society, vol. 91 (1959), pp. 1–52; vol. 108 (1963), pp. 106–142.Google Scholar
[5] MacQueen, D. B., Post's problem for recursion in higher types, Ph.D. Dissertation, M.I.T., 1972.Google Scholar
[6] Moschovakis, Y. N., Hyperanalytic predicates, Transactions of the American Mathematical Society, vol. 129 (1967), pp. 249–282.CrossRefGoogle Scholar
[7] Moschovakis, Y. N., Determinacy and prewellorderings of the continuum, Mathematical logic and foundations of set theory, North-Holland, Amsterdam, 1970, pp. 24–62.Google Scholar
[8] Moschovakis, Y. N., Abstract first order computability. I, II, Transactions of the American Mathematical Society, vol. 138 (1969), pp. 427–464; vol. 138 (1969), pp. 465–504.Google Scholar
[9] Moschovakis, Y. N., Structural characterizations of classes of relations, Proceedings of the 1972 Oslo Colloquium on Generalized Recursion Theory, North-Holland, Amsterdam, 1974, pp. 53–79.CrossRefGoogle Scholar
[10] Moschovakis, Y. N., Elementary induction on abstract structures, North-Holland, Amsterdam, 1974.Google Scholar
[11] Moschovakis, Y. N., On nonmonotone inductive definitions (to appear).Google Scholar
[12] Shoenfield, J. R., A hierarchy based on a type 2 object, Transactions of the American Mathematical Society, vol. 134 (1968), pp. 103–108.CrossRefGoogle Scholar
[13] Simpson, S. G., Post's problem for admissible sets, Proceedings of the 1972 Oslo Colloquium on Generalized Recursion Theory, North-Holland, Amsterdam, 1974, pp. 437–441.CrossRefGoogle Scholar