FORMALIZED RECURSIVE FUNCTIONALS
5
*28.1a,b. h b l o C - V ^ ^ b ) ^ 3) (b)
±
= o((i)+i] ~ V i R b ^ X ) 3 ( b ) ^ * ( i ) + l ]
#
*28.2. h o K *28.3 . F I k . *28.4. h pf ( i ) + 1 |rf .
*28.5. h a(x)|o(. *28.6. h blAi ( b )
±
- l . --28.6a. h 3cXb|tf.
PROOFS. *-28.1b. By *19.8 (FIM p . 35) .
**28.2, *28.3. By *19.6, *19.9a.
*28.4. By *19.9, *19.10.
*28.5. By *23.2, *23.3 .
*28.6. Assume (b).X. Using x 0 . 1 , and *6#7 with *138 (3K p . 188),
(Xi ( b ) ^ l ) ( i H l = ( ( b ) ^ l ) + l = ( b )
±
.
Next, l e t alb be a standard formula such tha t *-29.la holds; i t expresses
t h a t b as a representatio n of some values of ot i s an extension (proper or
improper) of th e representatio n ;a. Let "a., , . . . , a J b - . , . . . , b / , I f abbreviate
a
1
llb
1
& . . . & a^llb^.
*29.1a,b. h a||b - V i
i a
[ ( a )
±
0 3 ( a ) ^ ) ^ - Vi [(a)± 0 3 ( a ^ b ) , . ] .
•5'-29.2. f - 0||b. *29.3 . h Hlb. *29.4. h alia.
*29.5. h a | | 0 ~ a L . ---29.6. H aX & a||b D a l b .
*16.9. h bX & alb 3 ao. ---29.7. h bX & allb D ab.
*29.8. h allb & bile 3 allc. *29.9. h a||b & bloC 3 a|*.
-x-29.10. h x^r 3 £ ( x ) l l # ( y ) . *29.11. f - blod 0 b 113(b).
PROOFS. *29.5. I (=3). Assume alio. For - i - i n t r o d . , assume al .
Using #17.4 and -"-18.7, assume for successive 3-elims . Pr(p) & p | a , p=^?.,
P
±
WL. Now (a)
±
= ( p
i
c )
i
= ( p
i
)
i
+ ( c )
i
[*19.11, since aX)] = ( p ^ )
i
+ ( c )
i
£*3.6]
= l + ( c ) . [*19«9] 1 0. This with a||0 and *29.1 gives 0 (a) . = ( 0 ) . ,
contradicting *19.6. Hence (cf. IM Remark bottom p . 188) n a l , whence using
*139 aL. I I ( C ) . Use *29.2, -"-29.3. , . ,..
"x~29.6. I . Assume allb. We deduce | j .
k
p . | | | . , p . by induction
on k. BASIS. By *B3, t h i s reduces t o i l l , which we have by -"-153. BID. STEP.
^ (a) (a) . (a) (b) (b) (b)
By *Bk, I \±k,V± =C» l
i k
P
i
)-Pk a n d M
i k f P i
K l L ^ p . ).p
k
.
B u t ^ i k P i a '^i3cpi b y h7P* i n d - I f ^ k ^ 0 ' t h e n b ^ a | | b ^ V ^ k * S °
(a), (b). (a)r (b), ,
N
(a), y-
pk ^ k * so pk lpk by"*153'While if ^i?0' then Pk X hj ^tlf
Previous Page Next Page