FORMALIZED RECURSIVE FUNCTIONALS 9

proper index £, for given arguments su.,...,a, , (*.. , •.., ot £. The quantity to

be computed can be written " f(a.,...,§,, ^-,,.#., ^-0)" or showing £ explicitly

"{£](§n • • • *§ir ^i*•••**/)"• Such a computation with result w can be regarded

as a proof of~"^(a^,...,^,o^,...,^) ^w" or "ffKa^,...,^,^,,..,^^".

Our project will require us to treat formally such "proofs" or surrogates

for them* We imagine these "proofs" to be in tree form (IM pp. 106-107).

As we have already remarked (in 1.2), in the computation of

^(§-1*• • • QkQ(-i• * • &£) f°r particular a^,...,^,^,...,^, only finitely

many values of each of *n...,^C^ can be used; and finite inputs of

information about *-,,..., gCp can be represented by respective numbers

kv••**—£wnere ki*••• &£ I -l**•• 9^£*

In view of this, a proved statement n{£l(a-,,...,a, oCn*»*«c*i)a*w" can

replaced by a statement about four numbers, f, ka1,...,a, , J,b-.,...,b^

(where b^,...,b^l#-i,.#«,o(£) and w. The four numbers we combine into a

single quadruple number ^'^a_1 ,...,a, ,J,br.,...,bo,w. This number (in

appropriate contexts) will suffice to convey all the information conveyed by

the statement "ff](a.,,.•.,a,,oC-,...,oC n ) zz w". (Indeed, it conveys a little

more information, as it tells us that only values of s^,*...,^^ represented

in b. ,..•,b^ are needed.)

Using such quadruple numbers as"surrogates for the statements,we shall

now construe a computation as a computation tree, like a proof in tree form

(IM pp. 106-107), but with these numbers in place of statements or formulas.

The bottom position or lowest vertex will be occupied by the

quadruple number

£**%§-! • • • »2^9Ll2Li» • • • !£££

expressing the final result.

Applications of the eleven schema equations will constitute inferences,

with (SOb) (i.e.the second equation of (SO)), (S4) and (S5b) serving as

two-premise rules of inference, (SOa), (S5a), (S6) and (S3) as one-premise

rules, and (Si), (S2),(S3) and (S7) as zero-premise rules (or axiom

schemata).

Suppose, for example, that the final inference is by (SOb). In the

notation of 1.1, this means that we infer " ^(a^ir) ^ w" from " ^(a^^)^ u"

for some number u 0 and " ^(a1,^)~ w". Writing the variables now as