FORMALIZED RECURSIVE FUNCTIONALS
7
(S4), (S5),(S6) or (SB)£ is a proper index of the previously generated
function 4*, and that for (S4) or (S5) h is a proper index of the previously
generated function % (while for (S2) g can be any natural number, and for
(So) or (SB) h can be any natural number)• Since in each case the £ or the h
which must already be a proper index is smaller than the proper index of P
we have a course-of-values recursion defining the property of being a proper
index of some function. If only (Sl)-(SB) (but not (SO)) are used, we call
the proper index a primitive recursive index.
If a sequence of applications of (SO)-(SB) generating a function f (or in
the terminology of IM p. 220 or Kleene 1959 pp 3, 13, a description of tf by
these schemata) has been given, a proper index f of (f is determined. Suppose
the sequence of applications (or description) is irredundant; i.e. the
function introduced by each schema application except the last is used as the
^ or ^ of a later schema application (1959 1.4)* Then the proper index f
tells us what those schema applications are, except that it does not tell us
the numbers k and i of the variables of the two types which f takes (or the
numbers taken by the preceding functions).
This ambiguity is relatively harmless, and simplifies the proper
indices. From the aforesaid £ together with the original k and .£,we can
recover the original irredundant sequence of schema applications (generating
the original function f), except possibly for inessential details of the
order of the applications (e.g. whether prior to applying (S4)the ^ or the
% is generated first). If we use that f with other numbers k and £ of
variables, we get a similar sequence of schema applications, where if k or i
has been increased the function (p which is then generated is constant
in the additional variables of the respective type. If k or i has been too
much decreased, it may happen that, in the final or an earlier schema
application, the number of variables of the respective type which we are
supplying is fewer than the schema demands; in that case we interpret the
function introduced by that schema application (or "misapplication") as being
_
This recursion can be written in the manner of IM p. 233 Example 3 to show
the primitive recursiveness of this property. For the somewhat different
indices in 195Ba and in 1959 (which correspond to our proper indices),12 this
is done on p. 70 and p. IB respectively.
10The indices in Kleene 195Ba and in 1959 are more cumbersome, because they
also tell the numbers of variables.
Previous Page Next Page