The Basic Facts About HYP (1950-1960)
A set A c N, relation R c Nn or (total) function f : Nn ^ N is hyperarithmetical if it is recursive in some Ha; HYP is the set of all hyperarithmetical sets, and
To express succinctly (and prove) the basic properties of HYP-sets, it is useful to think of them as “bundled” with their codes by the following general notion:
Codings and Uniformities
A (surjective) coding of a set X is a pair (C, n), where n : C X is a surjection of the codeset C onto X, and we call any c e C a code (or name) of the object n(c) e X. If C c N, we say that the coding is in N. These are the only codings we will need for a while.
So (S), ||) is a coding of the constructive ordinals; (S), a ^ Ha) is a coding of the Ha-sets; (S), a ^ La) is a coding of Davis’ La-sets; and for a very elementary example, (N, e ^ ye) is a coding of the set of unary recursive partial functions. The coding of HYP we introduced by (5.23) is formally the pair
In practice we will never be so formal, in fact we will sometimes use codings which are “specified by the context” without a formal definition of C and n.
Codings are useful for expressing succinctly uniform properties of coded sets. Their general theory is technically messy, not very interesting mathematically and certainly not worth putting here.  We will confine ourselves to these remarks and “detail” sufficiently many claims to make the ideas clear. For example:
Lemma 5.3.1 HYP is uniformly closed under complements and relative recursion. In detail, there are recursive partial functions u (c) and v(c, e) such that:
- (1) If A is HYP with code c, then u(c) l and is a HYP-code of (N A).
- (2) Ifc is a HYP-code of a set B and A B, then v(c, e) l and is a HYP-code of A.
This is a simple lemma, as are the similar claims of uniform closure of the hyperarithmetical relations (with their natural coding) under all first-order operations on N. There is no use of effective effective grounded recursion in these proofs, we only need appeal to uniform properties of the jump operation like (5.15). The next result is also quite easy, but its proof requires effective grounded recursion and some auxiliary definitions on the constructive ordinals:
Lemma 5.3.2 HYP is uniformly closed under recursive unions.
In detail, there is a recursive partial function u(e) such that if ye is total and for each t, ve(t) is a HYP-code of a set At c N, then u(e) l and is a HYP-code of Lb At.
Two codings (Ci,n1), (C2,n2) in N of the same set X = n1[C1] = n2[C2] are equivalent if there are recursive partial functions u1(a), u2(b) such that
and similarly with 1 and 2 interchanged. It is clear that propositions like Lemmas 5.3.1 and 5.3.2 which hold uniformly for a certain coding also hold uniformly for every equivalent coding—and for some of them the proof might be easier. We exploit this idea by establishing an elegant characterization of HYP which produces a coding for it equivalent to the classical one in (5.23) but much simpler.
-  Cf. Moschovakis [36, 37] for a discussion (and many examples), and 7A.4 of Moschovakis for a specific result which codifies many of the applications of effective grounded recursion inDescriptive Set Theory.
-  The interested reader may want to look at Moschovakis  where it was necessary to developthis generalized abstract nonsense in some detail.
-  For a classical example, consider the coding of recursive partial functions specified by the NormalForm Theorem in App 5. Its precise definition depends on the choice of computation model thatwe use, Turing machines, systems of recursive equations or whatever, but all these codings areequivalent and so uniform propositions about them are coding invariant. §4.3-§4.5 of Rogers considers this situation in some detail and formulates stronger notions of equivalence than the onewe use.