Selection in abstract recursion theory
| Autor: | L. A. Harrington, D. B. Macqueen |
|---|---|
| Rok vydání: | 1976 |
| Předmět: | |
| Zdroj: | The Journal of Symbolic Logic. 41:153-158 |
| ISSN: | 1943-5886 0022-4812 |
| DOI: | 10.2307/2272954 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|