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
according to this rule
converges for a certain set A of n-tuples,
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.