Suppose a function *f* is defined recursively by

(1) { }

where is an expression that in general contains *f*. Suppose
that is the set of *n*-tuples for which *f* is
defined. Now let *g* and *h* be two other functions with the same
*domain* as *f* and which are defined for all *n*-tuples in . Suppose further that *g* and *h* satisfy the equation which
defined *f*. We assert that

for all in . This is so, simply because equation (1) uniquely determines the value that any function satisfying it has for arguments in which in turn follows from the fact that (1) can be used to compute for in .

We shall call this method of proving two functions equivalent
by the name of *recursion induction.*

We shall develop some of the properties of the elementary functions of integers in order to illustrate proof by recursion induction. We recall the definitions

Only the definition of addition and the properties of conditional expressions
were used in this proof.

*Proof* Define . It is easily seen that *f*(*m*,*n*) converges for all *m* and
*n* and hence is completely defined by the above equation and is
computable from it. Now

It is easily seen that the functions *g* and *h* defined by the equations *g*(*m*,*n*) =(*m* + *n*)' and *h*(*m*,*n*) = *m*' + *n* both satisfy the equation *f*. For example, it is
clear that and Therefore, by the principle of recursion induction *h* and *g* are equivalent functions on the domain
of where *f* is defined, but this is the set of all pairs of integers.

The fact that the above defined *f*(*m*,*n*) converges for all *m* and *n* is a
case of the more general fact that all functions defined by equations of the form

converge. We are not yet able to discuss formal proofs of convergence.

In presenting further proofs we shall be more terse.

*Proof* Let Again *f* converges for all *m*, *n*, *p*. We have

Each of these forms satisfies the equation for *f*(*m*,*n*,*p*).

Setting *m* = 0 in Theorem 3 gives

so that if we had 0 + *m* = *m* we would have commutativity of addition.

In fact, we cannot prove 0 + *m* = *m* without making some assumptions that
take into account that we are dealing with the integers. For suppose our space
consisted of the vertices of the binary tree in figure 2, where
#1#2#3#4#5@font#1#2pt#3#4#5

Fig. 2

*m*' is the vertex just above and to the left, and is the vertex
just below, and 0 is the bottom of the tree. *m* + *n* can be defined as
above and of course satisfies Theorems 1, 2, and 3 but does not
satisfy 0+*m* = *m*. For example, in the diagram 0 + *a* = *b* although *a*
+ 0 = *a*.

We shall make the following assumptions:

1.

2.

3.

which embody all of Peano's axioms except the induction axiom.

*Proof* By 3 and 4 as remarked above.

Now we shall give some examples of the application of recursion induction to proving theorems about functions of symbolic expressions. The rest of these proofs depend on an acquaintance with the Lisp formalism.

We start with the basic identities.

Let us define the concatenation of two lists *x* and *y* by the formula

Our first objective is to show that concatenation is associative.

*Th*. 11.

*Proof*

We shall show that and satisfy the functional equation

First we establish an auxiliary result:

Now we write

and

From these results it is obvious that both and satisfy the functional equation.

Let

NIL satisfies this equation. We can also write for any list *x*

which also satisfies the equation.

Next we consider the function *reverse*[*x*] defined by

It is not difficult to prove by recursion induction that

and

Many other elementary results in the elementary theory of
numbers and in the elementary theory of symbolic expressions are
provable in the same straightforward way as the above. In number
theory one gets as far as the theorem that if a prime *p* divides *ab*,
then it divides either *a* or *b*. However, to formulate the unique
factorization theorem requires a notation for dealing with sets of
integers. Wilson's theorem, a moderately deep result, can be expressed
in this formalism but apparently cannot be proved by recursion
induction.

One of the most immediate problems in extending this theory is to develop better techniques for proving that a recursively defined function converges. We hope to find some based on ambiguous functions. However, Godel's theorem disallows any hope that a complete set of such rules can be formed.

The relevance to a theory of computation of this excursion into number
theory is that the theory illustrates in a simple form mathematical
problems involved in developing rules for proving the equivalence of
algorithms. Recursion induction, which was discovered by considering
number theoretic problems, turns out to be applicable without change
to functions of symbolic expressions.

Wed May 1 17:18:52 PDT 1996