10 S. C.KLEENE

%••• 9^9 ^19• • • *£

^th-

£ °9 and showing theproper index £ « ®f£ 9 we

infer "(O^'Xa^,..?,^, ^,...,2^)^ if from "[^(^•••^^•••^^i) - H"

where u 0 and "KO^Tta^a^,...,^,oC1,...,oi%) ^w». Representingthe

statements byquadruple numbers,the"~bottom part ofthe tree (consistingof

the bottom vertex occupied bythe conclusion oftheinference, and two

vertices immediately over that occupied bythe premises) appears asfollows,

with k 0, forsome number u 0:

^^Sj^L* • • • %9l9\9 • • • *k^M2 09^ 9 ^9^19^2' • * • 9S^ 9L^1» * * * ^JT*^

«0,^,^,a1,...

9

^$Jj^9... #b^,w.

Similarly, ifthefinal inference isanapplication of (S5a),

£mss5$j&}£

and the bottom ofthetree (consisting ofthe bottom vertex occupied by the

conclusion, andone vertex immediately over that occupied bythe premise)

appears asfollows,with k 0:

g,qc-l,a2, .., ,^c,/,b1,.•.,bj,w

«5s^]39^0,a2,... ,ak,/,b1,...,b^,w#

As a third example, suppose thefinal (and only) step isanapplication

of (S7).Then f = 7 and the bottom (andwhole) ofthe tree appearsas

follows, where k 0, t 0, and (b-)Q 0 (sothat (b, ) "1isthe value,for

a..asargument, ofa function ot- such that b-l#,):

«7,k,a1,...

9

§t^f£p\, •.. ,bj, (feL)a~1.

Of course, these examples apply just aswell toanyother inferencein

the tree (instead ofthe final inference), reinterpreting thenotation tomake

^9^9±\9**°9$^9 Jb)h***)L$ 9?P the conclusion of that inference.

Let usreconsider the role ofthenumber £, assumed thus fartobea

proper index, inthe inferences. Fortheexample of (SOb), all that isreally

necessary isthat £ be ofthe form 0,g for some number g. That £ be a proper

index, sothat f will beone, isunnecessary, andwecanspare ourselves work

by not requiring that tobechecked aspart oftheinference inquestion.

Whatever effect £ exerts onthe computation will bethrough higher inferences

leading tothe two premises ofthis inference. Similarly, fortheexampleof

(S5a), itisonly necessary that f beofthe form 5,g,h g andh need notbe

proper indices.