14
S. C.KLEENE
Thence we canquickly derive thenormal form theorem (2.1 below, Kleene 1968).
Our main objective here is a formal theory, though itwill alsobe
important to recognize that it does formalize theinformal one. Fortheformal
theory, we seek a standard formula Gp(y) (FIMp. 27), containing free only y,
such that (1)rendered into theformal symbolism will be provable inthebasic
system of FIM (with thelist f0,...,f and Postulate Group D suitably
extended). Of course, Gp(y)will express Cp(v_)under theinterpretation.
Toward this end, we shall begin bywriting outCp~ (y),..»,Cp^(y) in the
formal notation using nCp(y),! fora formula still to bechosen.
From theforegoing discussion, thereader should recognize thate.g.
the formula Cp0,(y) shown below iswhat we getby expressing that y isa
computation tree number fora computation with final inference by (SOb),and
putting theresult informal notation. Butforourformal development, Cp0fc(y)
is theformula below simply by definition, forwhatever formula Cp(y)will
eventually be chosen tobe. Tc save space,we usethefollowingtwo
abbreviations "A"andf,B» (cf. m p. 224andFIMtopp. 29).
A T T ( y )o,i, i _ r r (*0o,2,i
A : ^ o , ! / * • B ! ^ o , ^ •
CPoJy): y=(y)0,(y)1 & c
P
((y)
1
) & (7)0flt0x &
(y)
0
=«o,(7)o,o,i ' A ' B ' ( 7 ) o,i,i &
(y)
1 0
=(y)
0 ) 0 A
, (y)
0 # 1
, (y)
0
,
2
0 
Cp^Cy): y=(y)
0
,(y)
1
,(y)
2
& CpCCy^) & c
P
((y)
2
) & (y)
0)10
o My)10f3o &
(y)
0
=«D,(y)o,o,i ' A ' B ' ( 7 ) o,3 &
( 7 ) 1 , 0  ^ 0 , 0 , 1 ' ( 7 ) 0 , 1 ' (y) 0,2 ( y ) l , 0 , 3 &
(y)
2 0
=(y)
0 j 0
,3 ( y )
0 j l
, (y)
0 2
, (y)
0
,
3

cp
1
(y): y=(y)o & (y)
010
0 &
(y)
0
=«L,A,B,(y)
0 A j l
'.
cp
2
(y): y=(y)o&
(y)
0
=«2, (7)0,0,1 ^ A ' B ' ( y ) o , 0 , 1 ^
cp
3
(y): y=(y)0 & ( 7 )
0 J 1 J 0
O &
( 7 )
0
= 5 ' A ' B ' ( 7 )
0 A ) 1
/