 # Myhill 

Two sets A, B are recursively isomorphic if one is carried onto the other by a recursive permutation of N, Myhill  introduces this notion and shows (among other things) that and so any two r.e. complete sets are recursively isomorphic. His methods also combine easily and to significant advantage with some of the results above: for example, Davis’ proof of (5.18) naturally gives the much neater However, none of Davis, Kleene or Mostowski knew of this article of Myhill when they wrote the papers we have been discussing.

# Effective Grounded Recursion

More significantly, neither Davis nor Mostowski refer or appeal explicitly to the following basic fact:

Theorem 5.2.3 (Kleene’s 2nd Recursion Theorem) For every recursive partial function f (e, x1,...,xn ,a1,..., am), there is a number e such that For recursion on N, this was stated unbilled and proved13 in the last two lines of §2 of Kleene  and it is the main technical tool that Kleene used for all his work on constructive ordinals, hyperarithmetical sets—and much more. Myhill  also used it, crucially, as did Spector  in his proof of the Uniqueness Theorem 5.2.2. Kleene and Spector use the 2nd Recursion Theorem to justify effective grounded recursion, which we can illustrate here with a relevant example.

Consider Davis’ definition of the sets {La : a e 51} which are his versions of the Ha-sets:

• (L1) L1 = 0,
• (L2) L2b = L'b, and
• (L3) if a = 3 ? 5e, then x e La (x)1 e He(xh.

Well, L1 is the complement of H1 and in the limit case Davis uses (x)1 and (x)2 rather than Kleene’s (x)0 and (x)1 which, together, don’t amount to much of a difference. The two definitions should be equivalent up to Turing equivalence, and they are:

Lemma 5.2.1 For every a e S1y Ha =T La. In fact, there are recursive partial functions u(a), v(a) which converge on S1 and satisfy The partial functions u(a), v(a) are uniformities which witness respectively the reducibilities Ha <T La, La <T Ha.

Proof The Turing equivalence Ha =T La should be more-or-less trivial by induction on the ordinal |a| and it is, when |a| is 0 or a successor ordinal (granting it for its predecessor). At a limit stage a = 3 ? 5e, however, there is no obvious way to put together the equivalences Het =T Let supplied by the induction hypothesis to prove that Ha =T La, and it is clear that we need to formulate a stronger, “uniform” proposition which will supply a usable induction hypothesis at limit stages. For the first reducibility in (*), one “recursion loading device” that works is the following:

Sublemma. There is a recursive partial function f (i, a, x) which converges for all i, x when i < 1 and a e S1 and satisfies the following: Proof of the Sublemma. We set f (0, 1, x) = 0 and f (1, 1, x) = 1. If a = 2b for some b, then f (0, a, x) = 1 and it is not hard to define f (1, a, x) from f (i, b, x) so that (**) holds using (5.15) in Footnote 6. Suppose now a = 3 ? 5e and (**) holds for all ordinals less than |a|. We compute the conditions that f (i, a, x) must satisfy by examining the equivalences which hold if it does: where we have used the induction hypothesis in the second line and the definition of La in the third (with an irrelevant 0 put into the first position so that f (1, a, b) codes a triple). So when a = 3 ? 5e we need to have Now, the 2nd Recursion Theorem easily supplies us with a recursive partial function f (i, a, x) which satisfies the relevant conditions for a = 1, a = 2b and (* * *), and then the proof is completed by a routine transfinite induction on |a |. ? (Proof of the Sublemma)

The corresponding Sublemma for the second reducibility in (*) is proved by a similar construction, and then the two Sublemmas together imply (*). ?

Briefly (and vaguely), to “compute” a function f : D ^ N which is defined on D c Nn by the recursion along some wellfounded relation -< c (N" x N"), we use the 2nd Recursion Theorem to find a recursive partial f which converges on D and satisfies (5.21) on the assumption that one such f exists; and then we prove by induction along x that f indeed satisfies (5.21). It is very important for the applications that no definability assumptions are needed for D or x, except as they might be used to define f; for the proof of Lemma 5.2.1, for example, and we have no estimate of the complexity of this D and this x, certainly not now.

The method is very general and we cannot do it justice here, but it has played a very important role in the study of hyperarithmetical sets and so I thought it important to give in full at least one proof which uses it. Another, similar but more difficult example is the uniform version of Spector’s Uniqueness Theorem 5.2.2: Its precise meaning is that there is a recursive partial function u(a, b), a uniformity, such that This formulation not only gives useful, additional information, but is necessary for the proof of the Uniqueness Theorem (by effective grounded recursion).

In the sequel I will often refer to effective grounded recursion and uniformity, but with little detail and less explanation.15 16

•  This strong uniqueness property cannot be extended to of, cf. Moschovakis , Nelson .
•  Choose k such that {k}(t, x, a) — f (S’m(t, t), x, a) and take e — S’m(k, k).
•  In the terminology of Post , the proof shows that Ha and La are equivalent by boundedtruth tables. Had Davis chosen to set L1 = N at the basis, then these modified La s are recursivelyisomorphic with Kleene’s Ha sets, and by a simpler argument than the proof of this Lemma. 