Relativization and the Kreisel Uniformization Theorem

We mention in App 6 the method of proof by relativization, which works because (roughly) recursion in some fixed parameters f has all the properties of “absolute” recursion. It is not simple to formulate a general metatheorem which captures all its applications—especially when uniformities are involved which should be “absolutely” recursive. It is, however, a very powerful method, heavily used by the early researchers in hyp theory, especially Kleene and Spector. We illustrate it here by proving two important and useful results.

The relative forms , П'кв, , A'f of the arithmetical and analytical hierarchies are defined simply by replacing “recursive” by “recursive in f” in their definitions, and they have all the properties of their absolute forms, including Lemma 5.1.1 (with absolutely recursive Sln,m functions).

The same is true for the relativized system Sf of ordinal notations: we simply replace et in Sect.5.2.1 by ef = {e}f (to) and write |a|f for the ordinal with code a e Sf. Markwald’s Theorem 5.2.1 remains true: an ordinal f is less than

exactly when it is the order type of a wellordering (of part of N) which is recursive in f. We use these ordinals to define the relativized Hf sets by replacing (H2) in Sect.5.2.2 by

(H2f) Hfb = jump (Hf; f) = {e : {e}(e, Hf, f);}

and we set

With these definitions, all the basic facts about HYP relativize, including Spector’s Uniqueness Theorem 5.2.2, the characterization of HYPf as the least о -algebra on N which is effective in f, Theorem 5.3.1 and the uniform inclusion HYPf c Aj’f, Theorem 5.3.3. For the converse inclusion (Kleene’s Theorem), we need to relativize the basic notions of Spector [47] : we set

Using these we get immediately the relativized versions of Lemma 5.3.6 and (what we need of) the relativized version of Lemma 5.3.7, basically (5.40):

(1) There are relations andin and nj respectively, such that for all в,

(2) If P (x, в) is П1, then there is a total recursive function f (x) such that

These suffice to relativize Spector’s proof of the non-uniform version of Kleene’s Theorem 5.3.4

and a little more detailed version of (2) gives also the uniform version.

With single sets rather than tuples of functions в, for simplicity, we set

The hyperdegrees that are induced by this reducibility have been studied extensively, cf. Sacks [46]. We will not go into this topic here, except for the following, early and important result. To appreciate what it says, notice that because W is nj-complete,

Theorem 5.3.8 (Spector [47]) For every set A c N,

and in relativized form, for all A, B c N,

Proof Suppose first that W ^h A and set

now ^ is a wellordering of rank m1 and it is A j a, so its rank is below SjA = mf- by the relativized version of Spector’s Theorem 5.3.5.

The converse is a bit easier. ?

Our second example illustrates a somewhat more subtle application of the rela- tivization technique: roughly, it proves a universal property )Q(fi) by treating

an arbitrary tuple в as a parameter, relativizing to it the proof of a simple (absolute) proposition, and then exploiting the uniform nature of the proof to infer Q(fi) with variable в.

Theorem 5.3.9 (П-Uniformization on N, Kreisel [27]) For every П relation P (x, y, в), there is a П relation P *(x, y, в) such that

It follows that if P (x, y) is П, then

Proof In the simple case where the list в of variables over N is empty, we choose a recursive g : Nn ^ N such that P (x, y) g(x, y) e W and set

I-

This also gives the second claim: check that if (Vx)(3y)P(x, y), then P*(x, y) is the graph of a function f and it is A, since

To get the more useful claim with parameters, we relativize this argument using () and (2) above. Given a П relation P(x, y, в), choose a recursive g(x, y) such that

and set

The check that this works is exactly as before. ?

TheKondo-Addison Uniformization Theorem for П relations P(x,a, в) (Kondo [24], Addison) is much deeper, but this simple result is also interesting and very useful.

 
Source
< Prev   CONTENTS   Source   Next >