In the previous section we presented a formalism for describing functions which are computable in terms of given base functions. We would like to have a mathematical theory strong enough to admit proofs of those facts about computing procedures that one ordinarily needs to show that computer programs meet their specifications. In [McC63] we showed that our formalism for expressing computable functions, was strong enough so that all the partial recursive functions of integers could be obtained from the successor function and equality. Now we would like a theory strong enough so that the addition of some form of Peano's axioms would allow the proof of all the theorems of one of the forms of elementary number theory.

We do not yet have such a theory. The difficulty is to keep the axioms and rules of inference of the theory free of the integers or other special domain, just as we have succeeded in doing with the formalism for constructing functions.

We shall now list the tools we have so far for proving relations between recursive functions. They are discussed in more detail in [McC63].

1. Substitution of expressions for free variables in equations and other relations.

2. Replacement of a sub-expression in a relation by an expression which has been proved equal to the sub-expression. (This is known in elementary mathematics as substitution of equals for equals.) When we are dealing with conditional expressions, a stronger form of this rule than the usual one is valid. Suppose we have an expression of the form

and we wish to replace *b* by *d*. Under these circumstances
we do not have to prove the equation *b* = *d*
in general, but only the weaker statement

This is because *b* affects the value of the conditional
expression only in case is true.

3. Conditional expressions satisfy a number of identities, and a complete theory of conditional expressions, very similar to propositional calculus, is thoroughly treated in [McC63]. We shall list a few of the identities taken as axioms here.

4. Finally, we have a rule called *recursion induction*
for making arguments that in the usual formulations
are made by mathematical induction. This rule may be
regarded as taking one of the theorems of recursive
function theory and giving it the status of a rule of
inference. Recursion induction may be described as
follows:

Suppose we have a recursion equation defining a
function *f*, namely

where the right hand side will be a conditional expression in all non-trivial cases, and suppose that

- the calculation of according to this rule
converges for a certain set A of
*n*-tuples, - the functions and
each satisfy equation (1) when
*g*or*h*is substituted for*f*. Then we may conclude that for all*n*-tuples in the set A.

As an example of the use of recursion induction we
shall prove that the function *g* defined by

satisfies given the usual facts about *n*!.
We shall take for granted the fact that *g*(*n*, *s*) converges
for all non-negative integral *n* and *s*. Then we need
only show that satisfies the equation for *g*(*n*, *s*).
We have

and this has the same form as the equation satisfied by
*g*(*n*, *s*). The steps in this derivation are fairly obvious
but also follow from the above-mentioned axioms and
rules of inference. In particular, the extended rule of
replacement is used. A number of additional examples
of proof by recursion induction are given in [McC63], and it
has been used to prove some fairly complicated relations
between computable functions.

Tue May 14 13:32:03 PDT 1996