FORMALIZED RECURSIVE FUNCTIONALS

13

The replacement of computations considered as proofs by these numbers

will help us in formalizing, since it is rather awkward to deal directly in a

formalism with metamathematical objects such as statements and proofs.

1.5. Let Cp(jr) = fy is a computation tree number^. In 1.4 we introduced

this.^predicate Cp(v_)by successive transformations, starting with the idea of

a computation as a proof in tree form, then replacing statements in such a

tree by quadruple numbers, and finally condensing the result to a single

number* Now we observe that an "intrinsic" definition of Cp^) can be given

entirely in number-theoretic terms. For, Gp(y) satisfies an equivalence of

the form

(1) Cp(£)= CP()a(y)V CPob(£) V ... V Cp8(y)

with eleven disjunctands Cp^(y),...,Cp^(y) on the right corresponding to the

eleven schema equations.

For example, Cp0,(y) expresses that £ is a computation tree number

representing a computation concluding with an application of (SOb) (the second

equation of (S0))# Thus Cp0,(y)must say that y is a number of the form shown

in the last display in 1.4, where (as stated there) the second and third lines

(minus the final "," or "") are smaller computation tree numbers. Now we can

easily express this condition on y in terms of the predicate Cp(y) itself

and the symbolism of the informal theory of primitive recursive functions of

IM Chapter IX supplemented by the notation n^Q,..#,a ". To begin with, since

y represents a computation concluding with a two-premise inference,

y = (][)()(l)~\ ^^o » where (y)-. and (y)2 are the smaller computation tree

numbers shown on the second and third lines, so Cp((y)-.) and Cp((y)?). Then

k,a,,#..,a, is (y)0 , , so the requirement that k 0 is expressed by

(y)0 - ,

n

0, etc. The complete expression to say that v _ is of the form

displayed last in 1.4 is shown below as Cp0,(y), but written in formal

notation (with a Roman "y" instead of an italic "y"); and similarly for each

of the eleven disjunctands in(1).

To get Cpf.(y),...,Cp^(y), of course we need only translate from the

formal notation used below into the informal notation. Yftie n all eleven

disjunctands are thus expressed, (1) can be recognized to be a

course-of-values recursion like that in IM p. 233 Example 3. So,by the method

of IM § 46 (based on Pe*ter 1934), Cp(y) is a primitive recursive predicate.