Go backward to 5.1 Inductive DefinitionsGo up to 5 Induction and RecursionGo forward to 5.3 Properties of Recursive Definitions

## 5.2 Induction as a Proof Technique

The Peano Axioms include for every formula F an axiom

(F[x <- 0] /\  (forall x in N: F => F[x <- x+1])) => forall x in N: F.

We may apply this axiom for proving properties of formulas involving natural numbers.

Proposition 64 (Mathematical Induction) In order to prove
forall x in N: F,
it suffices to prove
1. F[x <- 0],
2. (forall x in N: F => F[x <- x+1]).

In natural language, this proof strategy is usually indicated by the following triple of statements:

1. Induction Base: We show F[x <- 0].
2. Induction Hypothesis: We take arbitrary x in N and assume F.
3. Induction Step: We show F[x <- x+1].

Several examples are given below.

Example  We prove
forall n in N: n < 2n
by induction on n.

The induction base holds because 0 < 1 = 20.

Now we take arbitrary n in N and assume

(1) n < 2n.
We have to show
(2) n+1 < 2n+1.
By (1) we have
(3) n+1 < 2n+1
and therefore
(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1
which implies (2).

(The derivation of (2) from (1) and 1 <= 2n are knowledge that we assume granted in this proof).

Example  We prove
forall n in N: 3 | n3+2n
by induction on n.

The induction base holds because 3 | 0 and 0= 03+2*0.

We take arbitrary n in N and assume

(1) 3 | n3+2n.
We have to show
(2) 3 | (n+1)3+2(n+1).

By (1) and definition of | we have some a in N such that

(3) 3a = n3+2n.

We therefore have

 (n+1)3+2(n+1) = (n3 + 3n2 + 3n + 1) + (2n+2) = (n3 + 2n) + (3n2 + 3n + 3) = (3) 3a + 3(n2 + n + 1) = 3(a + n2 + n + 1)
which implies (2) by definition of |.

(In this proof we assume the computing rules in N as granted).

Example  We prove
forall n in N: (sum1 <= i <= n i) = (n+1)n/2
by induction on n.

The induction base holds because

(sum1 <= i <= 0 i) = 0 = (0+1)*0/2.

We take arbitrary n in N and assume

(1) (sum1 <= i <= n i) = (n+1)n/2.
We have to show
(2) (sum1 <= i <= n+1 i) = ((n+1)+1)(n+1)/2.

We have

 (sum1 <= i <= n+1 i) = (definition (sum )) (sum1 <= i <= n i) + (n+1) = (1) (n+1)n/2 + (n+1) = (n+1)n+2(n+1)/2 = (n+1)(n+2)/2 = (n+1)((n+1)+1)/2.
which implies (2).

(In this proof we assume the computing rules in Q as granted).

In particular, we can prove by induction the "computing laws" stated in Section natural numbers.

Example  We prove
forall x in N, y in N, z in N: x+(y+z) = (x+y)+z.
We take arbitrary x in N and y in N and prove
forall z in N: x+(y+z) = (x+y)+z
by induction on z.

We have by definition of +

x+(y+0) = x+y = (x+y)+0
and thus the induction base.

We assume

(1) x+(y+z) = (x+y)+z
and show
(2) x+(y+(z+1)) = (x+y)+(z+1).

We have

 (x+y)+(z+1) = (definition +) ((x+y)+z)+1 = (1) (x+(y+z))+1 = (definition +) x+((y+z)+1) = (definition +) x+(y+(z+1))
which implies (2).

Similar to inductive definitions with termination terms that are decreased by values greater than one, proofs by induction may use a more general induction rule which allows to rely on the truth of the formula to be proved for all predecessors of the current number.

Proposition 65 (Complete Induction) In order to prove
forall x in N: F
it suffices to prove
(forall x in N: (forall n < x: F[x <- n]) => F).

In complete induction, we use a generalized induction hypothesis in which we assume that F holds for all previous values of x (not just for x-1). There is no need for a separate induction base, because for x=0 the hypothesis (forall n < x: F[x <- n]) collapses to T.

The application of this proof strategy is usually indicated as follows:

1. Induction Hypothesis. We take arbitrary x in N and assume
forall n < x: F[x <- n].
2. Induction Step: We show F.

Complete induction can be applied not only in N but in every domain A with a well-founded ordering < subset A x A.

Example  We prove that every natural number greater than 1 can be factorized into a sequence of prime numbers, i.e.,
 forall n in N: n > 1 => (exists k in N, f: Nk -> N: n = (prod0 <= i < k f(i)) /\  forall i in Nk: f(i) is prime).
We proceed by complete induction over n.

We take arbitrary n in N and assume

 (1) forall m < n: m > 1 => (exists k in N, f: Nk -> N: m = (prod0 <= i < k f(i)) /\  forall i in Nk: f(i) is prime).
We have to show
 n > 1 => (exists k in N, f: Nk -> N: n = (prod0 <= i < k f(i)) /\  forall i in Nk: f(i) is prime).
We assume (3) n > 1 and show
(4) (exists k in N, f: Nk -> N: n = (prod0 <= i < k f(i)) /\  forall i in Nk: f(i) is prime).

If n is prime, then take k:=1 and f0 := n and we are done.

If n is not prime, then, by definition of primality, there exists some a with (5) 1 < a < n and (6) a | n. By (6) and definition of |, there exists some b such that

(7) a*b = n.
From (5) and (7), we have (8) 1 < b < n.

By (1) and (5), we have some ka in N and fa: Nka -> N with

(9) a = (prod0 <= i < ka fa(i)) /\  forall i in Nk: fa(i) is prime.
Likewise we have by (1) and (8) some kb in N and fb: Nkb -> N with
(10) b = (prod0 <= i < kb fb(i)) /\  forall i in Nk: fb(i) is prime.

Take k:=ka+kb and f(i):=if i < ka then fa(i) else fb(i). By (7), (9), and (10), we have

(11) n = (prod0 <= i < k f(i)) /\  forall i in Nk: f(i) is prime
which implies (4).

Similar to inductive definitions where the induction term may be a combination of the parameters, proofs by induction may proceed over the value of a term.

Proposition 66 (Induction over Term Values) In order to prove a formula F, it suffices to prove
(forall y in N: y=T => F)
where y is a variable that does not occur freely in T or F and T is a term that denotes a natural number.
To prove above formula, we may proceed by induction on y (using one of the variants described above).

In particular, in order to prove

forall x0, ..., xn-1: F
we may prove
(forall x0, ..., xn-1,y in N: y=T => F)

where T is a term with free variables x0, ..., xn-1. We can then take arbitrary x0, ..., xn-1 and prove (forall y in N: y=T => F) by induction on y.

Actually, we do not need an explicite variable y; it suffices to state

"we prove by induction on T"
and then proceed with an induction proof on the value of T (which must be a natural number). An example is given in the following section in the verification of Euclid's algorithm.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999