Abstract
The hyperarithmetical sets of natural numbers were introduced (independently) in the early 1950s by Martin Davis, Andrej Mostowski and Stephen Cole Kleene and their study is surely one of the most significant developments in the theory of computability: they have a rich and interesting structure and they have found applications to many areas of mathematics, including inductive definability , higher-type recursion, descriptive set theory and even classical analysis. This article surveys the development of the subject in its formative period from 1950 to 1960, starting with a discussion of its origins and with some brief pointers to later developments. There are few proofs, chosen partly because of the importance of the results but mostly because they illustrate simple, classical methods specific to this area which are not easy to find in the literature, especially in the treatment of uniformity; and these are given in the spirit (if not the letter) of the methods which were available at the time. This is an elementary, expository article and includes an Appendix which summarizes the few basic facts about computability theory that it assumes.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
cf. Moschovakis [32].
- 2.
- 3.
For example, Davis [4] proves that the set \(\{e :(\forall x)[\{e\}(x)\downarrow ]\}\) of codes of total recursive functions is in \(\varPi ^0_2\setminus \Sigma ^0_2\). The Hierarchy Theorem also yields a trivial proof of Tarski’s Theorem for \(\mathbf{N}\), that arithmetical truth is not arithmetical .
- 4.
He also said that “...with a few exceptions explicitly so noted, we have obtained formal proofs of all the consequently mathematical theorems here developed informally”, and it is clear that the purely intuitive approach can only go so far: we cannot hope to prove that (say) the word problem for semigroups is unsolvable on the basis of our intuitions about computability, without a rigorous definition of recursive functions and an appeal to the Church-Turing Thesis.
- 5.
For completeness, we will repeat in this section some parts of §7–§9 of Moschovakis [37], which goes over some of the same ground in more detail and includes several proofs.
- 6.
For example, to prove that \(K_k\) is \(\Sigma ^0_k\)-complete, you need the first of the following strengthenings of (5.10): there are recursive injections u(e, t), v(e) such that for all A, B and all e, t,
$$\begin{aligned} (1)~~\{e\}^A(t)\downarrow \iff u(e,t)\in A' \text { and }(2)~~A\leqslant ^T_e B \implies A'\leqslant ^1_{v(e)}B'. \end{aligned}$$(5.15)Proof: For (1), choose \(\overline{m}\) so that for any A, \(\{\overline{m}\}^A(e,t,y) =\{e\}^A(t)\) and set \(u(e,t) = S^2_1(\overline{m},e,t)\). For (2) you start with a recursive \(v_1(e)\) such that \(A\leqslant ^T_e B \implies \{e\}^A(t) = \{v_1(e)\}^B(t)\) and do a similar construction. That u(e, t) and v(e) are (absolutely) recursive injections—which has applications—depends on the fact that the functions \(S^{l,m}_n\) in App 5 are independent of any function parameters and injective, which I cannot find in any of the early texts (including Kleene [17]) even for \(m=0\).
- 7.
Spector [48] eliminates dramatically the most obvious approach at limit ordinals: No increasing sequence \(\mathbf d _0<\mathbf d _1<\cdots \) of Turing degrees has a least upper bound. Of course, this was not known to Davis, Kleene and Mostowski when they wrote these early papers.
- 8.
Kleene’s obtuse coding (the 3 and 5 in the definition) is motivated by the plans he and Church had to develop a general “constructive theory of ordinals ” beyond Cantor’s first and second number classes. They never got into this, but some (non-trivial and highly technical) results were proved by others, cf. Kreider and Rogers [25], Putnam [44], Enderton-Putnam [7]. We will not cover this topic here.
- 9.
O and \(\leqslant _O\) are defined by a (simultaneous) inductive definition as in App 10 which (in Kleene’s words) “is regarded from the finitary point of view as a correction, in that it eliminates the presupposition of the classical (non-constructive) second number class”. There are problems with this view, partly because many results about constructive ordinals cannot be proved (or even stated) without referring to ordinals. In any case, we will use \(\text {S}_1\) here.
- 10.
A proof of this basic fact is included in §8 of Moschovakis [37].
- 11.
For a discussion of the Spector Uniqueness Theorem and an outline of its proof for \(S_1\) see §9 of Moschovakis [37].
- 12.
- 13.
Choose \(\overline{k}\) such that \(\{\overline{k}\}(t,\varvec{x},\varvec{\alpha })=f(S^{1,m}_n(t,t),\varvec{x},\varvec{\alpha })\) and take \(e=S^{1,m}_n(\overline{k}, \overline{k})\).
- 14.
In the terminology of Post [42], the proof shows that \(H_a\) and \(L_a\) are equivalent by bounded truth tables. Had Davis chosen to set \(L_1=\mathbb {N}\) at the basis, then these modified \(L_a\)s are recursively isomorphic with Kleene’s \(H_a\) sets, and by a simpler argument than the proof of this Lemma.
- 15.
- 16.
The interested reader may want to look at Moschovakis [36] where it was necessary to develop this generalized abstract nonsense in some detail.
- 17.
For a classical example, consider the coding of recursive partial functions specified by the Normal Form Theorem in App 5. Its precise definition depends on the choice of computation model that we use, Turing machines, systems of recursive equations or whatever, but all these codings are equivalent and so uniform propositions about them are coding invariant. §4.3–§4.5 of Rogers [45] considers this situation in some detail and formulates stronger notions of equivalence than the one we use.
- 18.
A pointclass in this paper is any collection \(\Gamma \) of relations \(P(\varvec{x},\varvec{\alpha })\) with arguments in \(\mathbb {N}\) and \(\mathscr {N}\). It is an awkward term but useful, and is has been well established since the 70 s for collections of relations in various spaces typically specified by the context.
- 19.
They also suffice to prove that the notation system \(S_1\) is \(\varPi ^1_1\), cf. Lemma 1 in the proof of Theorem 9.2 in Moschovakis [37].
- 20.
What’s missing in their papers is the second part in the proof of the Boundedness Lemma 5.3.8 which looks tricky at first sight but is a standard, elementary tool in this area. It computes “witnesses to counterexamples” using diagonalization in very general circumstances, and we have already used it to establish the uniform properties of the jump in Footnote 6.
- 21.
Cf. App 9 for the notation we use about wellorderings and ranks.
- 22.
It is also his last paper on the subject.
- 23.
We need to include all arithmetical sets in \(\varDelta (\mathscr {F})\), ow. \(\varDelta (\emptyset )=\emptyset \) and \(\varDelta \) would close at 0 and build up the empty set.
- 24.
We assume some formal treatment of recursive substitutions into \(\mathsf A ^2\) formulas. In this case, the relevant recursive function is \((\alpha ,s)\mapsto (\alpha )_s\), and we use the equivalences
$$ \varphi (s,(\alpha )_s,\gamma )\iff (\exists \delta )[\delta =(\alpha )_s{~ \& ~}\varphi (s,\delta ,\gamma )]\iff (\forall \delta ) [\delta =(\alpha )_s\rightarrow \varphi (s,\delta ,\gamma )]. $$These are satisfied by every model \(\mathscr {F}\) of \((\varDelta ^0_\infty \text {-Comp})\).
- 25.
The converse fails, cf. Steel [51].
- 26.
- 27.
This is seriously implicit in §24 of Kleene [20], but the idea of the proof is there and Spector correctly credits Kleene for it.
- 28.
The “1” is necessary here, in fact it is not the case that every \(\varPi ^1_1\) set is the least fixed point \(\overline{\varPhi }\) of an arithmetical monotone operator \(\varPhi \) on \(\mathbb {N}\), cf. Feferman [8] and Moschovakis [34] (8.13, falsely claimed in the 1974 edition for all “countable acceptable structures”). Feferman’s result was the first applications of Cohen’s forcing to arithmetic.
- 29.
- 30.
Kleene [23] does not mention this and I recall him saying (much later) that he was not certain that the notion of a recursive partial function in higher type recursion was natural, but I cannot point to a reference for this.
References
Addison, J. W. (1959). Separation principles in the hierarchies of classical and effective descriptive set theory. Fundamenta Methematicae, 46:123–135.
Church, A. (1935). An unsolvable problem in elementary number theory. Bulletin of the American Mathematical Society, 41:332–333. This is an abstract of [3].
Church, A. (1936). An unsolvable problem in elementary number theory. American Journal of Mathematics, pages 345–363. An abstract of this paper was published in [52].
Davis, M. (1950a). On the theory of recursive unsolvability. PhD thesis, Princeton University.
Davis, M. (1950b). Relatively recursive functions and the extended Kleene hierarchy. page 723. Proceedings of the International Congress of Mathematicians, Cambridge, Mass, 1950.
Davis, M. (1965). The undecidable. Raven Press.
Enderton, H. B., and Putnam, H. (1970). A note on the hyperarithmetical hierarchy. The Journal of Symbolic Logic, 35:429–430.
Feferman, S. (1965). Some applications of forcing and generic sets. Fundamenta Methematicae, 56:325–345.
Gandy, R., Kreisel, G., and Tait, W. (1960). Set existence. Bulletin of the Polish Academy of Sciences, Series in Science, Mathematics and Astronomy, 8:577–582.
Gandy, R. O. (1960). Proof of Mostowski’s conjecture. Bulletin de l’Academie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques, 8:571–575.
Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica and verwandter Systeme, I. Monatshefte für Mathematik und Physik, pages 173–198. English translations in [53] and [54].
Kechris, A. S. and Moschovakis, Y. N. (1977). Recursion in higher types. In Barwise, J., editor, Handbook of Mathematical Logic, Studies in Logic, No. 90, pages 681–737. North Holland, Amsterdam.
Kleene, S. C. (1936). General recursive functions of natural numbers. Mathematische Annalen, 112:727–742.
Kleene, S. C. (1938). On notation for ordinal numbers. Journal of Symbolic Logic, 3:150–155.
Kleene, S. C. (1943). Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53:41–73.
Kleene, S. C. (1950). A symmetric form of Gödel’s theorem. Konin. Neder. Akad. van Weten. te Amst. Proc. of the Section of Sciences, 53:800–802.
Kleene, S. C. (1952). Introduction to metamathematics. North Holland Co: D. Van Nostrand Co.
Kleene, S. C. (1953). Arithmetical predicates and function quantifiers. Journal of Symbolic Logic, 18:190. abstract of a talk presented at a meeting of the Association for Symbolic Logic on December 29, 1952.
Kleene, S. C. (1955a). åArithmetical predicates and function quantifiers. Transactions of the American Mathematical Society, 79:312–340.
Kleene, S. C. (1955b). On the form of predicates in the theory of constructive ordinals (second paper). American Journal of Mathematics, 77:405–428.
Kleene, S. C. (1955c). Hierarchies of number theoretic predicates. Bulletin of the American Mathematical Society, 61:193–213.
Kleene, S. C. (1959a). Quantification of number-theoretic functions. Compositio Mathematica, 14:23–40.
Kleene, S. C. (1959b). Recursive functionals and quantifiers of finite types I. Transactions of the American Mathematical Society, 91:1–52.
Kondo, M. (1938). Sur l’uniformization des complementaires analytiques et les ensembles projectifs de la second classe. Japanese Journal of Mathematics, 15:197–230.
Kreider, D. L., and Rogers, H, Jr. (1961). Constructive versions of ordinal number classes. Transactions of the American Mathematical Society, 100:325–369.
Kreisel, G. (1961). Set theoretic problems suggested by the notion of potential totality. Infinitistic methods (pp. 103–140). Pergamon, New York.
Kreisel, G. (1962). The axiom of choice and the class of hyperarithmetic functions. Indagationes Mathematicae, 24:307–319.
Lebesgue, H. (1905). Sur les fonctions represéntables analytiquement. Journal de Mathématiques 6 \(^{\rm {e}}\) serie, 1:139–216.
Markov, A. A. (1947). On the impossibility of certain algorithms in the theory of associative systems. Coptes rendus (Doklady) de l’Academie des Sciences de USSR, 55:583–586.
Markwald, W. (1954). Zur Theorie der konstruktiven Wohlordnungen. Mathematischen Annalen, 127:135–149.
Moschovakis, Y. N. (1966). Many-one degrees of the predicates \(H_a(x)\). Pacific Journal of Mathematics, 18:329–342.
Moschovakis, Y. N. (1968). Review of four papers on Church’s Thesis. The Journal of Symbolic Logic, 33:471–472.
Moschovakis, Y. N. (1969). Abstract first order computability II. Transactions of the American Mathematical Society, 138:465–504.
Moschovakis, Y. N. (1974). Elementary Induction on Abstract Structures. North Holland, Amsterdam. Studies in Logic, No. 77. Republished by Dover Publications, Mineola, NY, 2008, with a correction to 8.3.
Moschovakis, Y. N. (2009). Descriptive set theory, Second edition, volume 155 of Mathematical Surveys and Monographs. American Mathematical Society.
Moschovakis, Y. N. (2010a). Classical descriptive set theory as a refinement of effective descriptive set theory. Annals of Pure and Applied Logic, 162:243–255.
Moschovakis, Y. N. (2010b). Kleene’s amazing second recursion theorem. The Bulletin of Symbolic Logic, 16:189–239.
Mostowski, A. (1947). On definable sets of positive integers. Fundamenta Methematicae, 34:81–112.
Mostowski, A. (1951). A classification of logical systems. Studia Philosophica, 4:237–274.
Myhill, J. (1955). Creative sets. Zeitschrifft für Mathematische Logik und Grundlagen der Mathematik, 1:97–108.
Nelson, G. C. (1974). Many-one reducibility within the Turing degrees of the hyperarithmetic sets \(Ha(x)\). Transactions of the American Mathematical Society, 191:1–44.
Post, E. L. (1944). Recursively enumerable sets of positive integers and their decision problems. Bulletin of the American Mathematical Society, 50:284–316.
Post, E. L. (1947). Recursive unsolvability of a problem of Thue. The Journal of Symbolic Logic, 12:1–11.
Putnam, H. (1961). Uniqueness ordinals in higher constructive number classes. Essays on the foundations of mathematics, pages 190–206. Magnes Press, Hebrew University, Jerusalem.
Rogers, Jr., H. (1967). Theory of recursive functions and effective computability. McGraw-Hill.
Sacks, G. E. (1990). Higher Recursion Theory. Perspectives in Mathematical Logic: Springer.
Spector, C. (1955). Recursive wellorderings. Journal of Symbolic Logic, 20:151–163.
Spector, C. (1956). On degress of recursive unsolvability. Annals of Mathematics, 64:581–582.
Spector, C. (1960). Hyperarithmetical quantifiers. Fundamenta Methematicae, 48:313–320.
Spector, C. (1961). Inductively defined sets of natural numbers. Infinitistic methods, pages 97–102. Pergamon, New York.
Steel, J. R. (1978). Forcing with tagged trees. Annals of Mathematical Logic, 15:55–74.
Suslin, M. (1917). Sur une definition des ensembles measurables B sans nombres transfinis. Comptes Rendus Acad. Sci. Paris, 164:88–91.
Turing, A. M. (1936). On computable numbers with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42:230–265. A correction, ibid. volume 43 (1937), pp. 544–546.
Van Heijenoort, J., editor (1967). From Frege to Gödel, a source book in mathematical logic, 1879–1931. Harvard University Press, Cambridge, Massachusetts, London, England.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Moschovakis, Y.N. (2016). Hyperarithmetical Sets. In: Omodeo, E., Policriti, A. (eds) Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Outstanding Contributions to Logic, vol 10. Springer, Cham. https://doi.org/10.1007/978-3-319-41842-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-41842-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41841-4
Online ISBN: 978-3-319-41842-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)