Home Mathematics Martin Davis on Computability, Computational Logic, and Mathematical Foundations
The main results from the period 1950-1960 that we have surveyed established HYP as a robust class of sets, those subsets of N which can be defined (and can be guaranteed to exist) if we accept the structure N of arithmetic, quantification over N and recursion. The main new method introduced in this work is undoubtedly effective grounded recursion, but there are also many interesting tricks, especially in computing “witnesses to counterexamples” as in the proof of Lemma 5.3.8.
There were primarily three developments which followed this work and are still extensively pursued today: recursion in higher types which we have already discussed and the following two.
IND and HYP on Abstract Structures
Of the many characterizations of HYP, the easiest to formulate for an arbitrary structure A = (A, R1,..., Rk) is Spector’s inductive definability in Sect.5.3.10, cf. Moschovakis . Briefly, a relation P c An is inductive in A if it is one of the mutual least fixed points of a finite system of positive, elementary (first-order) relations with arguments in A, and it is hyperelementary in A if both P and its negation An P are inductive.
Part of the theory of HYP and П can be developed for HYP(A) and IND(A) for arbitrary A; some of the results require an assumption that A is (almost) acceptable, roughly meaning that A admits a hyperelementary coding scheme for tuples; and suitable formulations of virtually all the results in the body of this paper can be established for all countable, acceptable structures, including Kleene’s centerpiece that IND(A) = П1 (A) and so HYP(A) = Aj(A).
Kleene’s Theorem 5.3.12 holds for all acceptable structures almost exactly in the form that it is stated in Sect. 5.3.9, with rn1 replaced by the closure ordinal k(A) of A, an important invariant. It is proved, however, by an entirely different argument which is different from (and perhaps simpler) than Kleene’s even for the classical structure N of arithmetic.
The proofs, in fact, are the most interesting aspect of this generalization of HYP theory: there is little coding and no use of effective grounded recursion. These are replaced by constructs which were first used in higher type recursion (Stage Comparison Theorems) and ideas from the theory of infinite open games.
The most interesting application of inductive definability is to the structure N2 of analysis in (5.31) which is intimately related to our last topic.
Effective Descriptive Set Theory
The term was coined by Addison  who formulated his results about the spaces Nn x Nm and might have still be thinking of “analogies” between the classical and the effective results; but in the 50+ years since then, effective descriptive set theory has evolved into a unified study of definability on recursive Polish spaces which include N, N and the real numbers and has deep applications to parts of topology and analysis in addition to classical descriptive set theory and logic. A good part of it is covered in Moschovakis , which, however, is concerned with many other things and is not sufficiently comprehensive on this topic.
|< Prev||CONTENTS||Next >|