# Kleene’s Theorem, HYP = A

This was the most important, early result about HYP and it is still the most fundamental.

Theorem 5.3.4 (Kleene [21]) A} c HYP, uniformly, so HYP = A}.

The foundational import of Kleene’s Theorem is that it reduces existential quantification (3a) over the continuum N to regimented iteration of first-order quantification over N—in the very special circumstances where a set A and its complement can both be defined by just one such quantification on arithmetical relations.

There are many proofs of Kleene’s Theorem, all of them ultimately based on the Normal Form Theorem 5.3.2 for П}} and using effective grounded recursion. The proof in Kleene [21] is quite complex and depends on several technical results about constructive ordinals and the Ha-sets. To outline briefly the much simpler argument in Spector [47] , put first

By Markwald’s Theorem 5.2.1, {|| f || : f e W} is exactly the set constructive ordinals, and we set

The first move is to check that the initial segments {f : f || < ||^||| of W are uniformly A for s e W:

Lemma 5.3.6 There are binary relations and <П in ?} and П respectively, such that

Proof Set

To verify that these relations do it, we code embeddings using elements of Baire space and use the closure properties of ? } and П. ?

The second move introduces what is now called the Kleene-Brouwer or Luzin- Sierpinski ordering on finite sequences. It is used in Kleene [2 1 ] and in many proofs of Kleene’s Theorem:

Lemma 5.3.7 (Spector [47]) W is П-complete, uniformly.

In detail: W is П and there is a recursive function u 1(a) such that if a is a nl-code of a set A c N, then ui(a) is injective and

Proof W is П1 directly from its definition. To show that it is П -complete, suppose that A is П1 with code a, so that by Theorem 5.3.2 and Lemma 5.3.5,

with a fixed recursive R(a, x, v) (not depending on A) which is monotone upward in its last argument. Define the transitive relation

and prove that

most easily by checking its contrapositive

We then linearize <a,x by setting verify that this is a linear ordering such that

in fact <a,x=^g(a,x) with a recursive g such that for any a, x, g(a, x) e L; and infer that

To finish the proof we need to define a recursive u1(a) such that {g(a, x)}(s) = [1] Most likely they did not even think of it: in the spirit of the time, a result was formulated uniformly only when this was necessary, typically in order to prove it by effective grounded recursion. Uniform claims did not become important in themselves until the 70s, when the applications of these ideas to Descriptive Set Theory made them necessary. We will discuss this briefly in Sect. 5.4.2.

Spector’s Lemmas 5.3.6-5.3.8 are important results with many applications besides their use in proving Kleene’s Theorem. We state one of them here and then one more, not quite so simple in the next section.[2]

Theorem 5.3.5 (Spector [47]) If < is a A wellordering with field F c N, then rank (<) < щ, uniformly.

This is usually abbreviated by the equation

5} being the least ordinal which is not the order type of a HYP wellordering.

Proof Suppose, towards a contradiction that A is a A wellordering with rank (A) > «1 and set

This is a Sj set and the hypotheses imply that A = W, which contradicts Lemma 5.3.8. The uniform version is proved similarly, using the uniform version of the same Lemma. ?

• [1] m1 (a)}(x)}(s) and {u1(a)} is injective for every a, and this is done by manipulating the Sln - functions as usual. ?

The third move is Spector’s. It is what makes his proof simpler than Kleene’s who worked with O rather than W.

Lemma 5.3.8 (Boundedness, Spector [47]) Every Ej subset of W is a subset of W% for some % < rn1, uniformly.

In detail: there is a recursive partial function u2 (b) such that if b is a ?}-code of a set A c N, then

Proof Let G(b, x) be a parametrization of the unary П relations by Lemma 5.3.5, so that a set A c N is Ej with code b if

Fix also by the nj-completeness of W a recursive injection g : N ^ N such that The relation

is Ej, and so by Lemma 5.3.5 again, there is a recursive injection v(b) = S2(k, b) (with some k) such that

The key observation is that

because if A c W and —G(v(b), v(b)), then there is some s e W such that g(v(b)) s; which gives g(v(b)) e W by Lemma 5.3.6; which in turn gives G(v(b),v(b)) by (*), contradicting the hypothesis. From G (v(b), v(b)) we get g(v(b)) e W,by(*) again, and so by taking negations in (**),

which is what we needed to show with u2(b) = g(v(b.b)). ?

Outline of proof of Theorem 5.3.4. By the two lemmas, if A is A1 with code (a, b), then

To complete the proof we need to show that W||f || is in B uniformly for f e W, and this is done by a fairly straightforward effective grounded recursion along {(f, g) : f, g e W & ||f|| < ||g||}. ?

Spector’s write-up of his proof is not quite this simple because he works with the Ha-codes rather than the B-codes of HYP and (in effect) proves the uniform inclusion B c HYP on the fly.

Moreover, neither Kleene nor Spector claimed explicitly the full, uniform version of Kleene’s Theorem 5.3.4, although all the “mathematical facts” needed for it are in their papers.{{What’s missing in their papers is the second part in the proof of the Boundedness Lemma 5.3.8

• [2] which looks tricky at first sight but is a standard, elementary tool in this area. It computes “witnessesto counterexamples” using diagonalization in very general circumstances, and we have already usedit to establish the uniform properties of the jump in Footnote 6.