Go backward to 5.1 Inductive Definitions
Go up to 5 Induction and Recursion
Go forward to 5.3 Properties of Recursive Definitions
|
Go backward to 5.1 Inductive Definitions Go up to 5 Induction and Recursion Go forward to 5.3 Properties of Recursive Definitions |
|
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.
forall x in N: F,it suffices to prove
In natural language, this proof strategy is usually indicated by the following triple of statements:
Several examples are given below.
forall n in N: n < 2nby 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+1and therefore
(4) n+1 < 2n+1 <= 2n+2n = 2*2n = 2n+1which implies (2).
(The derivation of (2) from (1) and 1 <= 2n are knowledge that we assume granted in this proof).
forall n in N: 3 | n3+2nby 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
which implies (2) by definition of |.
(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)
(In this proof we assume the computing rules in N as granted).
forall n in N: (sum1 <= i <= n i) = (n+1)n/2by 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
which implies (2).
(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.
(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.
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)+zby induction on z.
We have by definition of +
x+(y+0) = x+y = (x+y)+0and thus the induction base.
We assume
(1) x+(y+z) = (x+y)+zand show
(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.
forall x in N: Fit 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:
forall n < x: F[x <- n].
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 n.
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 take arbitrary n in N and assume
We have to show
(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 assume (3) n > 1 and show
n > 1 => (exists k in N, f: Nk -> N: n = (prod0 <= i < k f(i)) /\ forall i in Nk: f(i) is prime).
(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 primewhich 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.
(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.
In particular, in order to prove
forall x0, ..., xn-1: Fwe 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.