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.