THEOREM
*******
The principle of backwards induction:
ALL(a):[a e n
=> [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
where
n is the set of natural numbers
s is the successor function on n
P is any unary predicate
We can use the principle of backwards induction to prove that for all b in {0, 1, 2, ... a}, we have P(b). To do so, we need only prove:
(1) P(a)
(2) For all b in n and b<a and P(s(b)), we have P(b)
Informally, we start at the "end point" and work backwards to the "beginning."
Outline
*******
Line No. Description
1-6 Peano's Axioms
7-11 Properties of the < and <= relations used here
4-15 Define subset n' of n such that:
ALL(a):[a e n' <=> a e n & [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
16-26 Apply Induction Principle (PA5) from Peano's Axioms
27-46 Base case: Prove 0 e n'
47-114 Inductive step: Prove for all x e n', we also have s(x) e n'
115-End Generalizing, n'=n
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
PA1
2 0 e n
Axiom
PA2
3 ALL(a):[a e n => s(a) e n]
Axiom
PA3 (not used)
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
PA4 (not used)
5 ALL(a):[a e n => ~s(a)=0]
Axiom
PA5
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
Properties of < and <= relations used here
7 ALL(a):[a e n => [a<=0 => a=0]]
Axiom
8 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> a<b | a=b]]
Axiom
9 ALL(a):ALL(b):[a e n & b e n => [a<b => a<s(b)]]
Axiom
10 ALL(a):ALL(b):[a e n & b e n => [a<s(b) => a<=b]]
Axiom
11 ALL(a):[a e n => a<s(a)]
Axiom
Construct subset n' of n
Apply Subset Axiom
12 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [P(a)
& ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]]
Subset, 1
13 Set(n') & ALL(a):[a e n' <=> a e n & [P(a)
& ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
E Spec, 12
Define: n'
14 Set(n')
Split, 13
15 ALL(a):[a e n' <=> a e n & [P(a)
& ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
Split, 13
Apply Principle of Mathematical Induction from Peano's Axioms
16 Set(n') & ALL(b):[b e n' => b e n]
=> [0 e n' & ALL(b):[b e n' => s(b) e n']
=> ALL(b):[b e n => b e n']]
U Spec, 6
Prove: n' is a subset n
Suppose...
17 x e n'
Premise
Apply definition of n'
18 x e n' <=> x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
U Spec, 15
19 [x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]]
& [x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n']
Iff-And, 18
20 x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Split, 19
21 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n'
Split, 19
22 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Detach, 20, 17
23 x e n
Split, 22
As Required:
24 ALL(b):[b e n' => b e n]
4 Conclusion, 17
Joining results...
25 Set(n') & ALL(b):[b e n' => b e n]
Join, 14, 24
Sufficient: ALL(b):[b e n => b e n']
26 0 e n' & ALL(b):[b e n' => s(b) e n']
=> ALL(b):[b e n => b e n']
Detach, 16, 25
BASE CASE
*********
Prove: 0 e n'
Apply definition of n'
27 0 e n' <=> 0 e n & [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]]
U Spec, 15
28 [0 e n' => 0 e n & [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]]]
& [0 e n & [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]] => 0 e n']
Iff-And, 27
29 0 e n' => 0 e n & [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]]
Split, 28
Sufficient: For 0 e n'
30 0 e n & [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]] => 0 e n'
Split, 28
Prove: P(0) & ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]
Suppose...
31 P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
Premise
32 P(0)
Split, 31
33 ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
Split, 31
Prove: ALL(b):[b e n & b<=0 => P(b)]
Suppose...
34 x e n & x<=0
Premise
35 x e n
Split, 34
36 x<=0
Split, 34
37 x e n
Split, 34
38 x<=0
Split, 34
Apply property of <= relation
39 x e n => [x<=0 => x=0]
U Spec, 7
40 x<=0 => x=0
Detach, 39, 35
41 x=0
Detach, 40, 38
42 P(x)
Substitute, 41, 32
As Required:
43 ALL(b):[b e n & b<=0 => P(b)]
4 Conclusion, 34
As Required:
44 P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]
4 Conclusion, 31
Joining results...
45 0 e n
& [P(0)
& ALL(b):[b e n & b<0 => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=0 => P(b)]]
Join, 2, 44
As Required:
46 0 e n'
Detach, 30, 45
INDUCTIVE STEP
**************
Prove: ALL(b):[b e n' => s(b) e n']
Suppose...
47 x e n'
Premise
Apply definition of n'
48 x e n' <=> x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
U Spec, 15
49 [x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]]
& [x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n']
Iff-And, 48
50 x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Split, 49
51 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n'
Split, 49
52 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Detach, 50, 47
53 x e n
Split, 52
54 P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]
Split, 52
Apply definition of n'
55 s(x) e n' <=> s(x) e n & [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]]
U Spec, 15
56 [s(x) e n' => s(x) e n & [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]]]
& [s(x) e n & [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]] => s(x) e n']
Iff-And, 55
57 s(x) e n' => s(x) e n & [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]]
Split, 56
Sufficient: For s(x) e n'
58 s(x) e n & [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]] => s(x) e n'
Split, 56
Prove: s(x) e n
Apply PA2
59 x e n => s(x) e n
U Spec, 3
As Required:
60 s(x) e n
Detach, 59, 53
Prove: P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]
Suppose...
61 P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
Premise
62 P(s(x))
Split, 61
63 ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
Split, 61
Prove: P(x)
Apply premise
64 x e n & x<s(x) => [P(s(x)) => P(x)]
U Spec, 63
Apply property of < relation
65 x e n => x<s(x)
U Spec, 11
66 x<s(x)
Detach, 65, 53
67 x e n & x<s(x)
Join, 53, 66
68 P(s(x)) => P(x)
Detach, 64, 67
As Required:
69 P(x)
Detach, 68, 62
Prove: ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
Suppose...
70 y e n & y<x
Premise
71 y e n
Split, 70
72 y<x
Split, 70
Apply premise
73 y e n & y<s(x) => [P(s(y)) => P(y)]
U Spec, 63
74 ALL(b):[y e n & b e n => [y<b => y<s(b)]]
U Spec, 9
75 y e n & x e n => [y<x => y<s(x)]
U Spec, 74
76 y e n & x e n
Join, 71, 53
77 y<x => y<s(x)
Detach, 75, 76
78 y<s(x)
Detach, 77, 72
79 y e n & y<s(x)
Join, 71, 78
80 P(s(y)) => P(y)
Detach, 73, 79
As Required:
81 ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
4 Conclusion, 70
Joining results...
82 P(x) & ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
Join, 69, 81
As Required:
83 ALL(b):[b e n & b<=x => P(b)]
Detach, 54, 82
Prove: ALL(b):[b e n & b<=s(x) => P(b)]
Suppose...
84 z e n & z<=s(x)
Premise
85 z e n
Split, 84
86 z<=s(x)
Split, 84
Apply property of < and <= relations
87 ALL(b):[z e n & b e n => [z<=b <=> z<b | z=b]]
U Spec, 8
88 z e n & s(x) e n => [z<=s(x) <=> z<s(x) | z=s(x)]
U Spec, 87
89 z e n & s(x) e n
Join, 85, 60
90 z<=s(x) <=> z<s(x) | z=s(x)
Detach, 88, 89
91 [z<=s(x) => z<s(x) | z=s(x)]
& [z<s(x) | z=s(x) => z<=s(x)]
Iff-And, 90
92 z<=s(x) => z<s(x) | z=s(x)
Split, 91
93 z<s(x) | z=s(x) => z<=s(x)
Split, 91
Two cases to consider:
94 z<s(x) | z=s(x)
Detach, 92, 86
Case 1
Prove: z<s(x) => P(z)
Suppose...
95 z<s(x)
Premise
Apply previous result
96 z e n & z<=x => P(z)
U Spec, 83
Apply property of < and <= relations
97 ALL(b):[z e n & b e n => [z<s(b) => z<=b]]
U Spec, 10
98 z e n & x e n => [z<s(x) => z<=x]
U Spec, 97
99 z e n & x e n
Join, 85, 53
100 z<s(x) => z<=x
Detach, 98, 99
101 z<=x
Detach, 100, 95
102 z e n & z<=x
Join, 85, 101
103 P(z)
Detach, 96, 102
Case 1
As Required:
104 z<s(x) => P(z)
4 Conclusion, 95
Case 2
Prove: z=s(x) => P(z)
Suppose...
105 z=s(x)
Premise
106 P(z)
Substitute, 105, 62
Case 2
As Required:
107 z=s(x) => P(z)
4 Conclusion, 105
Joining results for Cases Rule
108 [z<s(x) => P(z)] & [z=s(x) => P(z)]
Join, 104, 107
109 P(z)
Cases, 94, 108
As Required:
110 ALL(b):[b e n & b<=s(x) => P(b)]
4 Conclusion, 84
As Required:
111 P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]
4 Conclusion, 61
Joining results...
112 s(x) e n
& [P(s(x))
& ALL(b):[b e n & b<s(x) => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=s(x) => P(b)]]
Join, 60, 111
113 s(x) e n'
Detach, 58, 112
As Required:
114 ALL(b):[b e n' => s(b) e n']
4 Conclusion, 47
Joining results...
115 0 e n' & ALL(b):[b e n' => s(b) e n']
Join, 46, 114
As Required:
116 ALL(b):[b e n => b e n']
Detach, 26, 115
Prove: ALL(a):[a e n
=> [P(a) & ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
Suppose...
117 x e n
Premise
118 x e n => x e n'
U Spec, 116
119 x e n'
Detach, 118, 117
120 x e n' <=> x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
U Spec, 15
121 [x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]]
& [x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n']
Iff-And, 120
122 x e n' => x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Split, 121
123 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]] => x e n'
Split, 121
124 x e n & [P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]]
Detach, 122, 119
125 x e n
Split, 124
126 P(x)
& ALL(b):[b e n & b<x => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=x => P(b)]
Split, 124
As Required:
127 ALL(a):[a e n
=> [P(a)
& ALL(b):[b e n & b<a => [P(s(b)) => P(b)]]
=> ALL(b):[b e n & b<=a => P(b)]]]
4 Conclusion, 117