Go up to 5 Induction and RecursionGo forward to 5.2 Induction as a Proof Technique |

We have introduced in Section 4.1 multiplication over **N** by the
following recursive definition (with termination function `r`(`x`,
`y`) := `y`)

*: NxN->Nx*y:=ify= 0then0elsex+(x*y^{-})

from which we can infer the following knowledge (Proposition *Natural
Number Operations*)

x* 0= 0, x*y'= x+( x*y).

or in another form

x* 0= 0, x* (y+1)= x+( x*y).

Actually also the inverse is true: this pair of equations uniquely determines
the function *: the first Peano law implies that the left hand side of only
one equation "matches" a particular application `a`*`b` (because
b is either 0 or `y`+1 for some `y` but not both) and the
second Peano law implies that argument b determines the value of parameter
`y` uniquely.

We can therefore write the definition also in the form

*: NxN->Nx* 0 := 0,x* (y+1) := x+(x*y).

The syntactic properties of these equations guarantee that the corresponding function is well defined.

where

f(x_{0}, ..., 0, ...,x_{n-1}):= T_{b},f(x_{0}, ...,x_{i}+1, ...,x_{n-1}):= T_{r}

for some termsf(T_{0}, ...,x_{i}, ...,T_{n-1})

If there exist `A`_{0}, ...,
`A`_{i-1}, `A`_{i+1}, ..., `A`_{n-1},
`B` with

then above definition introduces a function

forallx_{0}inA_{0}, ...,x_{i-1}inA_{i-1},x_{i}inN,x_{i+1}inA_{i+1}, ...,x_{n-1}inA_{n-1}:T_{b}inB/\T_{r}inB

such that the following holds:f:A_{0}x ... xA_{i-1}xNxA_{i+1}x ... xA_{n-1}->B

forallx_{0}inA_{0}, ...,x_{i-1}inA_{i-1},x_{i}inN,x_{i+1}inA_{i+1}, ...,x_{n-1}inA_{n-1}:f(x_{0}, ..., 0, ...,x_{n-1}) =T_{b}/\f(x_{0}, ...,x_{i}+1, ...,x_{n-1}) =T_{r}.

A function introduced by an inductive definition is uniquely defined.

One can generalize inductive definitions in various ways. For instance, it is
not necessary that the induction term is decreased by exactly 1. We may use
any non-zero decrement value as long as every possible case is covered by
a corresponding equation. For instance, in the definition of the
*Fibonacci Numbers (Fibonacci-Zahlen)*

we have two base equations because in the last equation the induction term

fib(0) := 1, fib(1) := 1, fib( x+2) := fib(x)+fib(x+1)

Furthermore, we may let the induction not just run over a single parameter but
over a *combination* of parameters as in

f(0, 0) := 0,f(x+1, 0) := 1+f(x, 0),f(x,y+1) := 1+f(x,y).

which defines a function that computes (in an artificially complex way) the
sum of both arguments `x` and `y`. In this case, the induction is
guarded by the *termination term* `x`+`y` whose value is
decreased by one in every recursive application of `f`.

If the induction runs over multiple arguments, we have to take special care that every possible argument pattern is covered by an equation. For instance, the definition

uses four equations to cover all possible cases.

f(0, 0) := 0,f(x+1, 0) := 1+f(x, 0),f(0,y+1) := 1+f(0,y),f(x+1,y+1) := 2+f(x,y),

The more complicated the recursive structure of a function definition is, the more important it becomes to show that a set of equations indeed defines a total function. This can be done by giving a termination term or, more general, by constructing a well-founded ordering.

We have

A(0,y) :=y+1,A(x+1, 0) :=A(x, 1),A(x+1,y+1) :=A(x,A(x+1,y)).

(e.g. <

x<y: <=>x_{0}<y_{0}\/ (x_{0}=x_{0}/\x_{1}<y_{1})

- <
`x`, 1>**<**<`x`+1, 0>, - <
`x`+1,`y`>**<**<`x`+1,`y`+1>, - <
`x`,`A`(`x`+1,`y`)>**<**<`x`+1,`y`+1>.

Also predicates can be defined inductively.

where

p(x_{0}, ..., 0, ...,x_{n-1}): <=> F_{b},p(x_{0}, ...,x_{i}+1, ...,x_{n-1}): <=> F_{r}

for some termsp(T_{0}, ...,x_{i}, ...,T_{n-1})

Above definition defines a predicate

such that the following holds:psubsetA_{0}x ... xA_{i-1}xNxA_{i+1}x ... xA_{n-1}.

forallx_{0}inA_{0}, ...,x_{i-1}inA_{i-1},x_{i}inN,x_{i+1}inA_{i+1}, ...,x_{n-1}inA_{n-1}:( p(x_{0}, ..., 0, ...,x_{n-1}) <=>F_{b}) /\( p(x_{0}, ...,x_{i}+1, ...,x_{n-1}) <=>F_{r}).

A predicate introduced by an inductive definition is uniquely defined.

We can define the same predicate also in the following way with two base cases and an induction term

iseven(0) : <=> T, iseven( x+1) : <=> ~iseven(x).

iseven(0) : <=> T, iseven(1) : <=> F, iseven( x+2) : <=> iseven(x).

Author: Wolfgang Schreiner

Last Modification: October 4, 1999