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

The Peano Axioms include
for every formula `F` an axiom

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

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

it suffices to proveforallxinN:F,

`F`[`x`<- 0],- (
**forall**`x`in**N**:`F`=>`F`[`x`<-`x`+1]).

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

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

Several examples are given below.

by induction onforallninN:n< 2^{n}

The induction base holds because 0 < 1 = 2^{0}.

Now we take arbitrary `n` in **N** and assume

(1)We have to shown< 2^{n}.

(2)By (1) we haven+1 < 2^{n+1}.

(3)and thereforen+1 < 2^{n}+1

(4)which implies (2).n+1 < 2^{n}+1 <= 2^{n}+2^{n}= 2*2^{n}= 2^{n}+1

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

by induction onforallninN: 3 |n^{3}+2n

The induction base holds because 3 | 0 and 0= 0^{3}+2*0.

We take arbitrary `n` in **N** and assume

(1) 3 |We have to shown^{3}+2n.

(2) 3 | (n+1)^{3}+2(n+1).

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

(3) 3a=n^{3}+2n.

We therefore have

which implies (2) by definition of |.

( n+1)^{3}+2(n+1)= ( n^{3}+ 3n^{2}+ 3n+ 1) + (2n+2)= ( n^{3}+ 2n) + (3n^{2}+ 3n+ 3)= (3) 3a+ 3(n^{2}+n+ 1)= 3(a+n^{2}+n+ 1)

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

by induction onforallninN: (sum_{1 <= i <= n}i) = (n+1)n/2

The induction base holds because

(sum_{1 <= i <= 0}i) = 0 = (0+1)*0/2.

We take arbitrary `n` in **N** and assume

(1) (We have to showsum_{1 <= i <= n}i) = (n+1)n/2.

(2) (sum_{1 <= i <= n+1}i) = ((n+1)+1)(n+1)/2.

We have

which implies (2).

( sum_{1 <= i <= n+1}i)= (definition ( sum_{}))( sum_{1 <= 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.

(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*.

We take arbitraryforallxinN,yinN,zinN:x+(y+z) = (x+y)+z.

by induction onforallzinN:x+(y+z) = (x+y)+z

We have by definition of `+`

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

We assume

(1)and showx+(y+z) = (x+y)+z

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

We have

which implies (2).

( x+y)+(z+1)= (definition +) (( x+y)+z)+1= (1) ( x+(y+z))+1= (definition +) x+((y+z)+1)= (definition +) x+(y+(z+1))

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.

it suffices to proveforallxinN:F

(forallxinN: (foralln<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:

**Induction Hypothesis**. We take arbitrary`x`in**N**and assume**forall**`n`<`x`:`F`[`x`<-`n`].**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`.

We proceed by complete induction over

forallninN:n> 1 =>( existskinN,f:N_{k}->N:n= (prod_{0 <= i < k}f(i)) /\foralliinN_{k}:f(i) is prime).

We take arbitrary `n` in **N** and assume

We have to show

(1) forallm<n:m> 1 =>( existskinN,f:N_{k}->N:m= (prod_{0 <= i < k}f(i)) /\foralliinN_{k}:f(i) is prime).

We assume (3)

n> 1 =>( existskinN,f:N_{k}->N:n= (prod_{0 <= i < k}f(i)) /\foralliinN_{k}:f(i) is prime).

(4) (existskinN,f:N_{k}->N:n= (prod_{0 <= i < k}f(i)) /\foralliinN_{k}:f(i) is prime).

If `n` is prime, then take `k`:=1 and `f`_{0} := `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)From (5) and (7), we have (8) 1 <a*b=n.

By (1) and (5), we have some `k`_{a} in **N** and
`f`_{a}: **N**_{ka} -> **N** with

(9)Likewise we have by (1) and (8) somea= (prod_{0 <= i < ka}f_{a}(i)) /\foralliinN_{k}:f_{a}(i) is prime.

(10)b= (prod_{0 <= i < kb}f_{b}(i)) /\foralliinN_{k}:f_{b}(i) is prime.

Take k:=`k`_{a}+`k`_{b} and
`f`(`i`):=**if** `i` <
`k`_{a} **then** `f`_{a}(`i`) **else** `f`_{b}(`i`).
By (7), (9), and (10), we have

(11)which implies (4).n= (prod_{0 <= i < k}f(i)) /\foralliinN_{k}:f(i) is prime

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.

(whereforallyinN:y=T=>F)

To prove above formula, we may proceed by induction on

In particular, in order to prove

we may proveforallx_{0}, ...,x_{n-1}:F

(forallx_{0}, ...,x_{n-1},yinN:y=T=>F)

where `T` is a term with free variables `x`_{0}, ...,
`x`_{n-1}. We can then take arbitrary
`x`_{0}, ..., `x`_{n-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 onand then proceed with an induction proof on the value ofT"

Author: Wolfgang Schreiner

Last Modification: October 4, 1999