COUNTABLE FUNCTIONALS AND THE ANALYTIC HIERARCHY

Dag Norma~~ Oslo 1977

Abstract V.Te work within the hierarchy of countable func-

. 2 1

tionals. We prove that 2-en(J+ w)

=

rrj(h1jr)(j?. 1) where h$

is some function recursive in ^{1jr •} We also prove that the associates for functionals of type j + 2 is a complete rr~ 1-set (j?. ^{0) •} This generalizes work of Bergstra [1]

J+

and [2]. In the end we prove that there is a functional 1jr Of type j + 2 ( j

?.

1) reCUrSiVe in Q I SUCh that

1-sc(1jr)Err~

-...r:

¹ . •

J J

1. Introduction.

Kleene [5] and Kreisel [6] defined independently the notion of countable (continuous) functionals. In this paper we will use a modified version of Kleene's definition. We will be interested in sets recursive and semirecursive in a given coun- table functional of a certain type. For the kind of problems we deal with, the modification is essential, as will be explai- ned through the results.

Kleene [5] defined the countable functionals of type k to be the elements of type k that when restricted to coun- table arguments act in a continuous way. This means that a countable functional takes both countable and non-countable arguments, they are elements of the maximal type-structure.

Kleene

[5]

also defines the associates for countable func- tionals. They are functions a : E ... lN that contains intentio- nal information about how the functional acts on countable

arguments. One disadvantage in regarding countable flmctionals as elements of the maximal type-structure is that two different functionals may have the same associates (which means that when restricted to countable arguments, they are identical).

In more recent papers on countable functionals it is nor- mal to regard the hierarchy of countable functionals, where a functional of type k + 1 is pnly defi~ed on counta9le ar-

~~0 See e.g. Bergstra [1] and Gandy - Hyland [3].

We may still use the notion of associate as defined in Kleene [5].

Before turning away from Kleene's original notion of countable functionals, we take a short look at recursion in a countable functional over the maximal type-structure. Our notion of recursion and semirecursion is derj_ved from Kleene' s 81 - 89 defined in Kleene [4] (Bergstra [1] has given an equi- valent definition). vve let

.2-envelo.Jle_ of )lr,

=

2-en ( 1j;) = fA <.::_

iP ;

^A is senirec·J.:&. ~lve in 1);!

1-section o:t:___j. = 1-sc ( ljr) = !A c JN ; A is recursive in

wl

For any countable functional 1jl there is a function hljr recursive in ljr with an associate a for ljr recursive in the jump of hljr ^vle use this observation (which is valid independent of which type-hierarchy we are in ) to prove

Theorem 1 (Kleene's original notion of countable functionals) a For any countable functional ¹⁾¹ there is an associate ~:~::·::·

for _$ recursive ^{j_n ~} 2, _1:!,

' .

b Let o. be an associate for countable functionals of type

;

tJ

.

Then there is a functional ~j recursive in a 2., _{' .c.}

with 0:. as nn associate.

c If j > 1 then 2-en($j+2 ) _{= TT} ¹ ₁ (h1p) d If j > 1 then 1-sc(1jsj+2 ) E rr 1 ¹ (h1jl)

All proofs are more or less implicit in the literature, and we just indicate them. (Bergstra [1] is a good source for them all)

a b

c

follows from the observation above.

Let a be an associate of a functional of type j + 2

.

For <:pj+1 define

r

recursive in 2

such that

any _{-cp cp' E}

if ~ is countable, then $cp is an associate for ~ •

If for some n,k,a(p(n));k+1 , we let 1js(cp) = k . Otherwis~$(~)=0

In this proof, let j+ 2

o

be the functional of type j+2 with constant value 0 • is recursive in

every set semirectrrsive in

v

will be semirecursive in h 2-cr j+20

1jl ' .J.;J' •

By a model-theoretic argument given in Moldestad - Normann [7] we see that

On the other hand, recursive in 1jl,hw

every ^TT

~

(h1jl )-subset of

JNIN

will be semi- Thus 2-en(1js)

=

^TT1 _{1 (h1jl)}

Remark In evaluating 2-en( tp) we only use on coun- table arguments, so by b it is fair to say that ~ is recursive in h$' E 2

d is a direct consequence of £ since

a E 1 - s c ( 1ji ) <::::::;> ::J e -..n { e } ( n, ^{1Jt )} = a ( n) and

{(e,n,a); {e} (n,$)

=

a(n)l is by c.

From now on we will work within the restricted hierarchy of countable f1.mctionals. Kleene' s 81 - 89 restricts smoothly to this narrowed hierarchy.

It is only natural that the notion of recursion will be somewhat different, since S8 is given a new meaning (we now regard functionals to be total when they in the old hierarchy were highly partial).

Bergst::-a [1] proves that if a is an associate for a

countable functional 1ji of type j + 2(j?. 1) , then 2-en(w) c

n~(a)

• In [2] Bergstra shows that if

v

is a functional of type

4,

then 2-en($)

=

n 2 (h1jl) 1 He also points out in [2]

a proof for the fact that 2-en(~)

=

ⁿ¹₁ ^{(h) when} _cp ^{~ is of}

type 3. As an immediate corollary of Bergstra's proof we see that the set of associates for countable functionals of type 3 is a complete

We will give a complete description of semirecursion over

:nP

relative to a co1.mta ble functional by the following result:

a If ^1)r is a functional of type j+2 , then b As(j+1) is a complete

n~-set

where A~. is the set of associates for functionals of type k •

This theorem answers a problem raised by J. Bergstra at the Generalized Recursion Theory II-conference in Oslo

-77.

As Bergstra points out in [2], if F is of type 2, then 2-en(F) ^{= TT} ~ (hF) , and if f is of type 1 , then 2-en(f) - l:~(hf)

=

L:~(f) , so we have described semirecursion at all levels.

We first observe that for the proof of Theorem 2,a it is sufficient to regard very simple functionals~ Let ko be the countable functional of type k that has constant value zero (This is not the same object as defined in the proof of theorem .:L_£) •

Lemma 1 If 2-en(j+ 2o)

=

rr~ , then

J

all

w

of type j+2 •

Proof: 2-en(•'•) c rr. ¹ (h*) c

't' · - J ^'t' 2-en ( j+2o ,hw c 2-en ) ( )

w .

for

We We also observe that it will be sufficient to prove that every L: . ¹ ₁-set

J- is semirecursive in j+ 2

o

since the subsets

'

of

ThiN

semirecursive in j+2

o

will be closed Q~der universal quantification over

nf'J .

Before going into any tech..11.ical details, we will give a short guide to the proof of theorem 2 and discuss some of the concepts involved.

The proof is essentially by induction on that As(2) is complete rr¹ 1 and we

is complete

may here

TT • 1 J-1 •

j • It is known assume that we have proved that As ( j)

Let B be l:j_ 1 1 Then there is a recursive map

such that

fEB<:$- a(f)t As(j)

We find a recursive relation S such that a(f)4 As(j) <~ V$j ::In S(f,w,n) and then

f E B <~~ ^{if $ j} ::In S ( f, $ , n)

Let q; be the partial, recursive function defined by P(f,$)

=

^{~n S(f,w,n)}

\WP (f, ~) will be total if and only if f E A , so

This shows that BE 2-en(j+ 2o).

be

In order to prove part b, we let A L:. 1 1

J- such that

be TT ~

J and let B

f E A ~ ^'V g ( f , g) E B ~-:;:. ^if gV$ j ::In S ( ( f , g) , \If, n)

By pairing g and $ , we may find a recursive relation

s

1 such that

Letting

rO if ::In

s

₁^(f,$,n)

9?(f,$) -

J

- lundefined otherwise

we reduce A to As(j+1) by mapping f onto an associate for A.~9(f,tlr)

Now, let us look at the idea behind the definition of S • To each functional ~ we define uniformly recursive in ^t1r

By comparing {a;a(a)

=

o! with

KS(~) for various t1r , we will be able to tell if a is an associate. An unprecise definition of KS(~) could be:

Given a with sequence number k . If ^cr may be extended to an associate, we find an extention Yk that takes value k+1 as often as reasonable (here we will follow an idea from Kleene

[5]).

Let the functional with associate be

(or rather $~ where J is the type). We define KS by

6 E KS(t!r) if and only if W($lc) ⁼ k •

The properties of this definition that are most usefull will be

i and

i i k1 ~ k2 -~ $, ~ tlrk

.Lc1 2

ili If w (a) (cp)

+

^{(a) ~ then a 11decides lr} the value ~ (cp)

\'within reason ^a when w has an associate extending a • Now S will compare to what extent {a: a(~)(a)

=

o}~KS($) . We will be more precise later.

Before turning into the real proof, we need some

2. Conventions an~~inolo£Y.

We identify sequences and sequence-numbers. a,T,o,TI will denote sequences or sequence-numbers, i,j,k,l,m,r,s, will

denote natural numbers, f,g,h,a,~,~ will denote functions;

the Greek letters will be used in connection with associates.

F,G will denote fm1ctionals of type 2 and ~,w,P and !

f~~ctionals in general. A superscript j will indicate the type.

In order to avoid confusion we may assume that all numbers are sequence-numbers, and we let lcrk}kE~T be the identity-

enumeration of sequences (So by our convention, crk

=

k).

If a= (k , ••• ,k 1o n-

>

we will without mentioning use that

cr > k. for all i = 0, ••• ,n-1 and a > n = lh(cr) • Vie write

l

cr(i) for ki , and for a function f , we write f(n) for (f(O), ••• ,f(n-1)) •

By

gJl] __ =

~ we mean that for some m cr(f(m))

=

n+1 • If for no n,o(f)

=

n we say that

£1fl

is undefined. We will only use this terminology when n is unique.

All functionals we construct will have canonical associates, and if ~ is a functional of type j we write cr(~)

=

n

if for the cannonical as so cia te x for ~,o ( t ) = n

We will use terminology from Kleene [5] and it will be an advantage to lmow §§1-2 from that paper. In particular we will use

Conj(rr 1,rr 2) <-> There is an element ~ of type ^j such that both rr 1 and rr 2 may be extended to associates for ~ •

is defined if Con j (rr 1, rr 2) , and then An extj(n,rr 1 ,rr2 ) defines an associate extending rr 1 for the fm1ctional ^cp

We let

mentioned in the definition of Conj

be the functional with associate ).n ext j ( n ;rr 1 , ^TI 2 ) •

It follows from the definition in Kleene [5] that Extj(rr 1,rr 2 ) = Extj(rr 2 ,rr 1) • Kleene proves that the relations Conj and the

functions extj are primitive recursive, and it is implicit in his proof that the functionals Extj(rr 1,rr2 ) are uniformly recursive in rr 1 ,rr 2 •

We will now make some of the concepts from the introduction more precise.

Definiton 1 For superscript j we assume that Conj(rr) a ^j

=

¹

j

=

2

. > 2

~=

is defined

=

~IT 1 k( t) --

'

{

rrk(t) if rr(t) otherwise

= frrk(f) if rr(f)

l

^otherwise

is defined

r

^s if for some ,. we have Conj- 1('1) , rr('T)=s+1 and for all a,cr 1 , if

. 2 1 1

Con J- (cr ,a ) ;-r (a) > 0 and cr ~ lh{rr)

i

then cp(Extj- 2 (cr ,cr 1 ).,-(cr )-1 k otherwise

Remark All these f~uLctionals will be uniformly recursive in n, k • The functional Wj is based on the same idea as

TT,k

Kleene's Extj(rr) • It is fairly stright-forward to prove that W~ k(cp) is uniquely defined. A sufficient argu.rnent is fou.."Yld in the proof of lemma ' 5.

b Let These are the functionals discussed in the introduction.

c If ~ is of type j+1 , we let the ~!7 set of ~ be

d If cp is a functional of type j-1 , we say n(cp) =. s (potentially)

if for all kE]iJ'

wJ

^k(cp)

⁼

^S,

'

_!{.ema;r-k n(cp) will take s as a potential value if vre never used the ¹¹otherwise¹¹-case in defining W~ k(cp) • The motivation for this definition is that we will need to foretell the value '

111 (cp) from TT when cp has an associate that extends n • If w has an associate a such that rr(a) is defined, this

foretellingshould be correct, and moreover it should be recur- sive. If n(cp)

=

s (potentially) we foretell in a recursive

way that w(cp)

=

s • (There is no guarantee for stating 1jl(co)

=

s from n(cp)

=

s (potentially), unless ^{TT (} cp) is defined as

If

11:~

k(cp) 4= k

'

then n(cp) has

111~

^{k( q))}

. '

^n(cp) will never have more

'

~emax:k We may now define hljl by If

w

is of type j + I , let

a potential value, than one potential

above).

namely value.

2_.

hw

^(cr)

=

^{.. ~-}_\

I

\_ 0 othervdse

Proof of theorem 2.

---~·JW=Ot'•

... ..--...

By induction on j ~ 1 we are going to prove that

Induct~on g~othesis

For each n ~ set ^A c ~ there is a recursive relation

J R such that

ii For each

Di For each f there are n₁ ~ n 2 such that R(f,n1) and R(f,n2)

We showed in the introduction how to prove Theorem 2.a from part

1

of the induction hypothesis. Theorem 2.b will be proved as a corollary at each induction step (see lemma

4).

ii. and -~ are technical parts of the induction hypothesis, and will only be used in lemma 3.

Jn_duction ~Si.2, _i

=

1 This proof is just a reformulation of the argument given by Bergstra [2]. We could have used his proof directly as an induction basis, but that would require a nonuniform formulation of the induction hypothesis.

Lemma 2 Let nE As(2) (locally). Then the following

.,

__

^{,_,._.. ....}

two statements are equivalent.

i For some F ~ {a; u(cr)

= ol

^c: KS(F) ii a.E As(2)

Proof Assume {cr; cr(a)

= o!

^{c KS(F) • Let f} be a func- tion. We prove that for some m,u(f(m)) > 0 by showing that for some m, "f(m) ~ KS (F) •

Let

p

be an associate for F and choose m₀,k such that

then

p(f(m

_{0 ))}

=

k+1 • Now, if m > m₀ and f(m)E KS(F) , F(fJ(m)) = :f'(m) (as a sequence-number) ^{o By} definition of f"f(m) as an extention of f(m) , ff(m)(m_{0 )}

=

f{m_{0 )}

Thus F(~f(m))

=

k , so f(m)

=

k ^o

There is atmost one m1 > m₀ such that f(m_{1 )}

=

k . Then

for m > m1 , ·I(m)

$

KS(F) , so a(f(m)) > 0 • This proves

i -:::> ii •

Now, assume that uE As(2) . We let a

< 'I<

^f mean that a is a subsequence of ^'I which again is• of the form f(m) • Define

F(f)

=

k if a(crk)

=

0 and for some ^'I et(T) > 0 , crk

<

^'I

<

^{f and 'I ~ fk}

0 otherwise

i.e. we check for each crk

<

f such that a(crk) ⁼ 0 if f looks like fk up to the least n such that a(f(n)) > 0 • Then we let F(f)

=

k •

We must prove that F is well defined. If F(f)

=

_{k 1}

and F(f)

=

_{k 2} ~ choose n oinioal such that a(f(n)) > 0 f(n) is an extention of crk by k 1 and an extention of

1

crk by _{k 2 ,} and since both extentions are proper, we see that

2

f(n)

=

k₁ and f(n)

=

k_{2 •} Then k₁

=

_{k 2 ,} which proves that F is well defined.

F is countable since it is recursive in a • If a(crk) = 0 it is clear that F(fk) = k , so crkE KS(f) •

This proves ~l >

i·

We may now prove the induction basis:

Let A E r-r 1 ₁ Let S be a recursive tree such that fE A <e ~ Vg 3n-, S(1(n),g(n),n)

For each f E

ifT

let

(o

if lh(cr) < 1 or S ('f (lh( cr))

,a,

^lh(cr))

' j

l L1

^otherwise

a.f E As(2) (locally) and

By lemma 2

Let

d

R(f,n)

<=>

af(cr_{11 )}

=

⁰

i and

11

in the induction hypothesis are clearly satisfied.

ldi

is satisfied since aj{cr)

=

0 if lh(cr) ~ 1 •

This ends th~ proof of the induction basis.

The inductio~_st2~·

We now assume that the theorem is proved for all ^{rr. 1} sets.

J

1 ~1.

Let A E Tt j+ 1 and let B be ^~J such that fE A<?> Vg (f,g) E B

By the induction hypothesis there is a recursive relation _{R1 ,} satisfying jl and ~~i, such that

so

. 1

f E A <·"'> V gV $ J + 3n ( _{R 1 ( (} f, g) , n) & an~ KS (

ir ) )

If we let $

1

^(~)

=

$((j0,~)) and gW(n)

=

^{$(j(n+1)) (where}

jk is the type j functional with constant value k ) we see that

We will now for each f try to define an ¹¹associate¹¹ for the functional that to each $j+¹ gives ⁰ if there is an n such that

If

R1 ((f,gw) ,n) & an~ KS(iJ_{1 )}

. 1

ConJ+ (a) we say that a

-

contains sufficient infer-^{- ----~~~}

mation about iJ to compute w(~) when there is a canonical associate y for ~ and a(y) is defined.

~~k. For each n, when we check if R1((f,g$),n)

&

an~ KS($ 1) holds, we only apply ^$ to fm1ctionals Cf the type jk,~~ or variations over these, for which we have canonical

associates.

pef~on~~ If Conj+ 1(cr) we use the following Fecursive procedure to find aj(cr) •

Go to the least n such that Conj(crn) and i or ii below hold~

i cr does not contain enough information about $ to evaluate the truth of _R1((f,g$),n) or to compute

w1<wR)

ii cr does contain this information~ R1 ((f,g~),n) and

"'1<wR) ~

^{n .}

If this least n satisfies i let

--'

satisfies

li,

let a~(cr)

=

^{1 •}

Remark will be the associate for the partial func- tional we described above. If cr

<

^T and af(cr)

=

1 , then af(T)

=

1 by the same verification.

We will prove that af is total for all f , and thus locally an associate. af takes values 0

there are no conflicting positive values.

and 1 only, so

. 1

If ^I Con J+ (cr) we may let af(cr)

=

0 •

~~mma ~ For each f and cr , if is defined.

. 1

Con J+ (cr) , then af(cr)

Proof.

---=

Let cr 1 be the part of an associate for w₁ we may extract from cr • There are two cases:

i 9"-4{(

>2 >_g.

Pick extending cr •

w1

w

such that w has an associate will be constant, say ,,, - j+1k

'~'1 - •

that

•

Choose n 1 ^~ n2 such that

·W~ may.assume that :n1 ^~ k .• since

a contains sufficient information to state this. By}:.} .. in the induction hypothesis, Con ^{j (a ) ,}

n1 so if for no _{' n} satisfies i or ii, certainly n₁ will satisfy

11·

ii ~~-~=~Q (or is undefined)

It is sufficient to prove that a

1

^(w~) is undefined for some n , since then i will hold for this n •

Let a

=

(k+1).

nk Any functional with an associate ex- tending a will be

nk jk , so in particular

(constant value

k).

some k since a ₁ undefined.

Now is undefined for

is finite, so

a 1 ^(w~ )

^{will be}

k

We prove theorem 2.b and end the first part of the indue- tion step by~

Lemma 4.

Proof. . ^~ __,.,-.

.

functional $ for some n •

Let f E A , ~ E As ( j + 1 ) be an associate for a

To establish~ we will show that af(~(n)) = 1

Since f E A it follows from ( 1) that

Let n₀ be the least such n • For a number of functionals

~1^{, ••• ,~}1 we compute $(roi) (i

=

1, ••• ,1) in order to verify

this property of n₀ • Let y_{1 , •••} ,y₁ be canonical assiciates for t+>1 , ••• ^,c~1 .

Pick m so large that ~(m)(yi) are defined for i = 1, ••• ,1 This is possible since

pE

As(j+1) • But then af(~(m))

=

1

since S(m) contains sufficient information about ~ to compute ~(~1 ^), ••• ,$(~1⁾ and thereby verify the property of

<:: Assume that f ~ A • Then by ( 1) there is a functional 'IJt

for which

Let 13 be an associate for ^{1ls •} If af (ff(tl))

=

1 for some m ~ this means that ~(m) contains enough information about

w

to ensure that for some n

which is impossible. Thus a-'-'(p(m)) = 0 for all m , and

J..

af is not an associate.

To end the proof of the induction step we will give a higher type versj_on of Lemma2 for the af' s • There are some obstacles that prevent us from giving the same argument with- out modifications. One of these is that we may have a pair

ak

<.,.

such that af(crk) == O,af(.,-)

=

1,.,- may be extended to

an associate for w~+i but .,. never takes the value k+1 • (See the proof that F is well defined in Lemma 2). If this is the case, crk will contain enough potential information to indicate that we do not need the value k from 'Wj+i to

k

ensure that

(Potential computations are defined in Definition 1.d).

We will see that it is sufficient to regard those crk for which wo need the value k from 111~+¹ • We make this property precise in the following definition~

Defin~ti~~-2 The function £l--i£f P,Otentiall~) is defined as af with the difference th~t we demand cr(~) (potentially) where we in the definition of af would demand that cr con- tains sufficient information to compute ^~(~) .

Bema~~· By the argument of lemma 3 we may also show that a~ is total.

If ^a.(cp)

=

^k

'

then cr((())

=

^k (potentially). This shows that if a+-(cr) .1..

=

_{1 ' then} a~ (cr)

=

¹

.

Both functions af and aP

f will be uniformly recursive in f

.

In general {cr ~ ai(cr)

= ol

will not be a tree, and af is not an associate even locally. .P

\!fe are now going to prove that

(2) is an associate ~ 3~ J "+2 Vn(Con J• (an) . '1 & af(cr p _{11 )}

=

0

( -i+ 1

If we let R(f, n) ~~ Con·-' (a )

n and

~ a " :r ... E KS ( !li ) ) •

a:g(cr )

=

0)

1 n we see that i and ii. in the induction hypothesis is established.

. 1

To see part iii, note that if an= (0, ••• ,0) then ConJ+ (cr_{11 )} and a¥ (crn)

=

0 (crn contains no information at all).

~ in (2) will be established through lemmas 5 and 6, while ~is proved in lemma 7. For later use, lemma 7 will

t ...

be a bit too strong for this proof.

f_§,.rprn.a ?_. Let ^tp be a functional of type j and let

!JE As(j+1) . If for some n,k 1 and k2

13 (n) (cp) = k 1 (potentially) and ~"(n+1) (cp) = k 2 (potentially)

Proof. If j=1 , this is trivial since potential and real computations are the same. So assume that j > 1 •

According to definitions 1.a and d, choose ,- 1 such that . 1

~(n)(,-1 ⁾ = k 1+1 and such that when T1

(o)

> 0, ConJ-

(o,o')

and

o'

^~ n ' then

Choose ,- 2 for f-i"(n+1),n+1 and k 2 inasimilarway. Itis sufficient to prove Conj(T

1

^~,-

2

^{) , since}

Conj+ 1(F(n+1)) & W(n+1)(~

1

^{) = k 1+1 & ~(n+1)(,-}

2

^{) = k2+1}

& Conj(,- 1,,.2 ) ~ k 1 = k2 by Kleene's definition of C'onj+ 1 from [5].

So choose rr 1,rr 2 such that Conj- 1(rr 1,rr 2 ),,-.1(rr 1) > 0 and ,- 2 (rr 2 ) > 0 • According to Kleene [5], we must prove

that ^T 1 ( ^TT 1 ) ^{= ~} 2 ( ^TI 2 ) •

B(n+1)(~2⁾ is defined, so ,- 2

s

ⁿ _{and rr 2} ^{< n . Clearly}

rr 1 < n • Then by choice of ,- 1 and ,-2

This proves the lemma.

Lemma 6 Let ~ be of type j+2 and assume that

Then af is an associate.

Proof Let p E As ( j+ 1) . As in the parallell part of lemma 2 we may conclude that there is an n such that for no

m

>

n ~~(m)E KS(~) •

By assumption

m > n ~ a~ (~"(m)) ⁼ 1 •

In order to obtain a contradiction, assume that for no m ~ n,af(~(m)) = 1 •

In the verification of a~(~(n)) ⁼ 1 we demand potential values ~(n)(~) for certain functionals ~ . Since ~ is an associate, ~(m)(~) will be defined for some m • But the real and potential values cannot be the same for all ~

occuring in the verification of a~(~(n)) ⁼ 1 , since otherwise there would be an m > n such that af(~(m))

=

1 •

Thus there must be a first place in the verification of a¥(iJ'(n)) = 1 where for some cp , 13 (n) (co) is demanded,

~(n)(~) has a potential value s , but for some m > n

~(m)(~) does not have potential value s •

By lemma 5, for the least such m , p(m)(cp) has no potential value at all. By the choice of ~ we would demand the poten- tial value of

p(m)(~)

in order to compute

a~(!3(m))

^{, and}

would get a~(j3(m)) ⁼ 0 • This contradicts the assumption, and the lemma is proved.

~emm~_T If af is an associate then there is a functional

~ uniformly recursive in f such that

R£££f:

We give the following algoritho for computing {li(w) :

Find the least n such that _{R 1} ((f,g'lji) ,n) & crn ~ KS($ 1 ) • For a finite sequence of functionals ~1^{, ••• ,~}1 we

evaluate w(~1), ••• ,~(~1) in order to verify this property of n • Now, if for some crk,a~(crk)

=

0 and 11r and

W~+¹ agree on ~

1

^{, ••• ,~}

1

^{, we let ~($) =} k. Otherwise we let ~($) - 0 •

Through claims 1-3 we will prove that ~ is well de- fined, recursive in f and satisfies the inclusion above.

9lai~. If ^1lr agrees with a~ (crk)

=

^{0 ,} then for some i <

•lr j+ 1 on 'i'k

1 w c~.) _]. =

~1, ••• 'cpl k .

Proof: As we pointed out after Definition 1, if

and

W~+

¹

(cp) =

s

t

^{k ,} then

crk(~) =

s (potentially). If for no

i ~ _{_} ^{1 , 11r}_{'I'-~ 1}^Jr.+1(Ml.) _'+' ^{= k} we o a1.n po en la va ues crk bt · t t• 1 1 ( ^~i ) for all i < 1

..

^By choice of cp 1 ' ••• '~1 we see that a~(cr k)

=

¹ contradicting the assumption. Thus w<~i) ⁼

w~+1(cpi)

=

k for some i < n

By this claim we see that to compute _~ Cw) we only need to check if a¥(crk) = 0 and _1lr agrees with ^11rj+1

k on

~1' ••• '~1 for k E { W ( cp 1 ) , • • • , ^{1jJ (} cpl )

l

^{Thus ~ ( 1lr)} is defined by a recursive instruction.

Claim 2 If qi(1jr)

=

k1 and \li(w)

=

k2

,

then ^k 1

=

k2

.

J'.E..CL o J.. Vve may assume that ~Cw) is not defined by the

otherwise case. Assume k1 < k2 • By claim 1 ' $(cpi)

=

k2 for some i < 1 But w(cpi)

=

^1jrj+1 _k1 ^(cp.)

l ~ k1 for all i < 1

.

This gives a contradiction •

. ~). If a.¥(crl';) = 0 then crkE KS(~)

P ^f B th 1 ·thm f ~('lrkj+¹ ) , the value 1·s k ._too.-.:..;,. y . e a gor1 or ...

since af k P(cr )

=

0 and ~.j+•k ¹ agrees with itself on ^rn ~1, ••• ,~1 ^rn · This ends the proof of lemma

7,

and Theorem 2 is established •

. 4-._.QrL ..

:~..he J:s~cti2lL.2 ..

=L ..

a co1E!.ta 91e funcyl..onal.

We recall that the 1-section of 1jr will be 1-sc(w)

=

{f ; f is recursive in

tf

As in the proof of Theorem 1.d. we see that . ( j+2) 1( )

1 - s c 1jr E TT j h$

Also 1-sc (F) E TT

~

^{(hF) .}

In Normann [8] we proved that there is a co1..mtable func-

tional F of type 2 recursive in 0' such that 1-sc(F) E ^{TT 1} 1 ^'i:1 1 In this section we extend this result to arbitrary types by

proving

Theore~2. ( j

?.

1)

There is a countable functional 2 of type j+2 recursive in 0' such that

a For j 2 there is a 1-obtainable functional wj+1 such that for all ~j

1-sc(~) ~ 1-sc($)

b There is no "plus-one ^1' theorem for co1-mtable fu..'lction<:l.ls.

c (Bergstra [ 1]) ]¹or each j = 2 or j > 3 there is a non-reducible 1-obtainable functional of type j •

(Bergstra proved this for j = 3 as well).

d There are functionals

w

of any type such that JiliN'\ 1-sc(w)

is not semirecursive in

w •

Remark. A function2,1 is 1-obtainable if it is recursive

...,,..

__

._,_,..._--.-..

in a function.

A "plus-one theorem¹¹ would say tbat for all k > 2 and all wk there is an I' such that 1-sc(F)

=

^1-sc(wk)

Sacks [11] and [12] :proved plus-one theorems for normal functionalo in the maximal type-structure.

~ indicates that in gener~l there is no gap in complexity between the 1-section and the semirecursive relations (There cer- tainly is a gap in complexity between the recursive and semi- recursive relations). As a curiosity we mention that adding 2E will alter this picture completely. (It makes good sense to do recursion in a countable functional and 2E as long as we do not apply the functional on discontinuous arguments).

0 2

By arguments from Theorem 1 we can prove that 1-sc(wJ, E)

=

2 1

1-sc(hw, E)Err 1(h$)

In Normann [8] we constructed the functional by letting it

11climb¹¹ a long wellorded set of r.e. degrees. The production of the 1-section was a rather slow process. The functional

we will construct to prove Theorem 3 will produce it's 1-section in a more hastily way.

Proof of th~:r:e~

We will use a result from ordinary degree-theory, proved by a finite priority argument. The method used in the proof of this proposition is found in most introductions to degree- theory, and it is a slight improvement of the wayo Friedberg and Muchnic solved Post's problem (see e.g. Rogers [1],

Sacks [10] or Sboenfield [13])

;pro.J2.o&,tion

There is an r. e. set B c ::N x JN such that for no mE JH

where Bm

=

{k; (m,k)E B}

B_m

= !

(n,k) E B

. _,

_{m ~}

_n!

Now, let .A~]I:J be rr~

J

.

^Vle will construct a fnnctional iJi of type j+2 such that

mE A ~ Bm E 1-sc(iJi)

If 1-sc(iJi)E l:J.; , we see that AE

!::.; ,

so we may choose A not to be t::,~ and thereby prove theorem 3.

By the proof of Theorem 2 there is a. recursive relation

R such that

where we by lemma 7 may choose 1)r recursive when mE A • Let S be recursive such that

(m,k) E B ~ :3s(s,m,k) E S

Let ~ be the functional of type j+2 defined by

~(1)r,m,k)

r

I 1

= -} I

if :3s[(s,m,k) E S & Vn

:'5

s(R(m,n)~ onE KS($))]

: 0 otherwise

Lemma 8 ~ is recursive in B and thus COQ~table.

~ro2f:. To compute ~(1)r,m,k) from B , ask ::Js(s,m,k) E S (i.e.. (m,k) E B ?)

If no , ~(t,m,k)

=

0 • If yes, let s₀ be the least such s and ask if the following hold~

If no, ~(1)r,m,k)

=

0 , if yes ~(1)r,m,k)

=

1 •

then Bm is recursive in ~ • yroofJ. Let 1jr be recursive such that

Then

~(1jr,m,k)

=

1 <--> 3s(s,m,k)E S ~ (m,k)E B

and Ak~($,m,k) is the characteristic flli~ction of Bm Lemma 10. If m

4

A

0 then is recursive in

-.,-:. . ^{- -} ....

Proof: We show hO\•T to compute q>($,m,k) from

~~..-... -.. ~ ...

If m _=I= mo we act as in lemma 8.

If m

=

mo

'

then mEfA and 3n(R(m,n) & crn4 KS($))

Let n₀ be the least such n • Now

I 1 if 3s <n (s,m,k) E

s

} ⁰

cr($,m,k) = ^J \

I i

if Vs < n₀ (s,m,k)

4

S

I 0

I ~

This proves the lemma.

B -mo B_m •

0

•

Now, if m4 A,B _m cannot be recursive in since it then will be recursive· in B

-m by lemma 10.

By choice of B this is not the case. This ends the proof of theorem 3.

Bern~. By turning the argument from theorem 3 upside down, we see that cr is recursive in B_m if and only if m ~ A • This shows that the relation

ipj+2 is recursive in f

is not a

rr~-relation.

This should be no surprise since the most natur~l definition of this relation, given an asEociate

for cr , will be by a TI . 1 _J+ 1-formula.

REFERENCES

1. J. :Sergstra, Computability and continuityinfinite types, Disertation, Utrecht 1976.

2. J. :Sergstra, 1-Envelopes of Continuous Functionals, Re- cursive Function Theory: Newsletter No 16 (1977) Item 196.

3. R.O. Gandy and J.M.E. Hyland, Computable and recursively countable functions of higher type, in R.O. Gandy and J.M.E. Hyland (ed3) Logic Colloquium 76 407-438, North-Holland 1977.

4. S.C. Kleene, Recursive Fm~ctionals and Quantifiers of Finite Types I, Tran.Amer.Math.Soc. 91 (1959) 1-52;

and II 108 (1963) 106-142.

5. S.C. Kleene, Com~table functionals, in A. Heyting (ed):

Constructivity in Mathematics, North.:.:.Holland (1959) 87-100.

6. G. Kreisel, Interpretation of Analysis by means of Con- structive Fu..11ctionals of Finite Types, in A. Heyting (ed): Co structivity in Mathematics, North-Holland (1959) 10 -128.

7. J. Moldestad and D. Normann, Models for recursion theory, Journal of Symbolic Logic 47 (1976) 719-729.

8, D. Normann, On a problem of S. Wainer, Oslo Preprint

Series No 13, 1976. To appear in Journal of Symbolic Logic ^m~der title;

9. H. Rogers Jr., Theory of Recursive Fm~ctions and Effective Computability, l\1cGraw-Hill 1967.

10. G.E. Sacks~ Degrees of Unsolvability, Annals of Nathema- tical studies~ Princeton University Press, 1963.

11. G.E. Sacks, The 1-section of a type n object, in

J.E. Fenstad and P.G. Hinman (eds) Generalized Recursion Theory (North-Holland,Amsterdam 1974) 81-93.

12. G.E. Sacks~ The k-section of a type-n object, to appear.

13. J.R. Shoenfield, Degrees of Unsolvability, ~~thematics

Studies 2, North-Holland/ Amerj_can Elsevier 1971.