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
Previous Page Next Page