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