6 S.C.KLEENE
(a)k (b)
so by--'16.3 Pk 'Pic - . Soweget what weneed for the ind. step by*l6.4.
II. Now assume also aX). Ifb=0,then alb by—L6.1; sosuppose bX). Now
TT
^i TT ^ i
(since aX), a = I l±ap± [-19.16J = I 'i
n a
x(a b)P± tb7amax(a,b)
(-8.4), *B15, ia=(a).=0 (-19.8),X3.1,and*B13lI. Similarly (sincebX)),
(b). 1 T-r ^ i T T ^ i
b=TTinax(a,b)Pi ' *• But TTitoc(a,b)Pi N Jin«(a,b)Pi b^
substituting max(a,b) for k inthe result of I. Soalb.
--1.6.9. (Numbered tofitinFIM top p. 28.) Use -143a.
-29.7. Assume bX)& a lib0 Ifa=0, abisimmediate. Soassume aX).Now
by -29.6, alb. Soby-16.9 (here), ab.
-29.8, -29.9. Expanding I I andI by-29.1a,b and-28.1a,b,theproofs
become clear.
-29.10, -"-29.11a Straightforward, using *23.2 and-23.3.
Now (and again in1.5) weshall augment thelist f0,...,f offunction
symbols andPostulate Group D, asweleft open the possibility ofdoing in
FIM 5.1 H Here weintroduce o asa new function symbol (which is f2«,
since o£(x)ofFIM p. 38is f ^ ' wi*11the axiom X30»1 (which fits (a) of
FIM p . 20).
max((a).,(b). )
x
3
0 . 1 . a o b = n
i I i a x ( a b ) P
. X X . -30.2 . I - aob=*oa.
- 3 0 . 3 . I- al* & blot D aobl* & allaob & blaob.
-30.4 . h Vi
±
^
b
C(a)
i
,(b)
±
0 3 ( a J ^ C b ) ^ o allaob & blaob.
PROOFS. - 3 0 . 3 . Assume aloe and bloc. I . To deduce aob lad via - 2 8 . 1 ,
assume (aob).X). If iiiax(a,b), we would have (aob).=0 by 30.1 with -19.13 ;
so imax(a,b). Hence by -19.14, (aob).=max((a)./b).). Now i f ( a ) . ( b ) . , then
0 (a°b). = max ( ( a ) . , ( b ) . ) = (a) , [by - 8 . 2 ] , so by ale* (with -28.1) (aob). =
(a)
±
= oC(i)+l. Similarly i f ( b ) . ( a ) . , (aob).= *(i)+l. So aobl*. I I . To
deduce allaob, assume ia and (a).X). Then by alcx, (a).= ctf(i)-fl. By ia,
imax(a,b); so (as under I) (aob).=max((a).,(b).) . Now i f ( a ) . ( b ) . , then
(a)
±
= m a x ( ( a )
i
, ( b )
i
) = (aob)
±
, as desired . If (b)
±
(a)
±
0, then (a) . =
oC(i)+l = ( b )
i
[by bloc] = m a x ( ( a )
i
, ( b ) . ) = (aob). , again. I I I . We deduce
b || aob symmetrically.
SL-. a
1.3o Let ^Q,..»,a = £Q ••••#ErrT"as ^ F-^ P# 92e-tc# ^ e n-umber shown
at the right opposite each oftheschemata (S0)-(S8) in1.1we shall call a
proper index ofthe function dp, provided that for(an application of)(SO),
Previous Page Next Page