THEOREM
*******
Suppose we have the finite set m = {0, 1, 2, ... xn}. We can prove that, for all x in m, P(x) is true by proving:
(1) P(xn)
(2) For all non-zero x in m, if P(x) then P(x-1).
Informally, we start at the "end point" (xn) and work backwards to the "beginning" (0) proving P is true for each element of m.
More formally, we establish here the principle of backwards induction:
ALL(a):[a e n
=> [P(a) & ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
where
n is the set of natural numbers
P is any unary predicate
Outline
*******
Line Nos. Description
14-17 Construct subset n' of n such that:
ALL(a):[a e n' <=> a e n & [P(a) & ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
18-28 Apply the principle of ordinary induction to prove n'=n
29-46 Base case: Prove 0 e n'
47-141 Inductive step: Prove x e n' => x+1 e n'
142-154 Generalizing
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
AXIOMS
******
n is a set (the set of natural numbers)
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
Define: + operator on n
4 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Define: - operator on n
5 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a-b=c <=> a=c+b]]
Axiom
0 is less than any successor of a natural number
6 ALL(a):[a e n => 0<a+1]
Axiom
Ordinary induction on n (with + operator)
7 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => b+1 e a]
=> ALL(b):[b e n => b e a]]]
Axiom
Properties of < and <= relations used here
8 ALL(a):[a e n => [a<=0 => a=0]]
Axiom
9 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> a<b | a=b]]
Axiom
Useful properties of < and <= relations on n used here
10 ALL(a):[a e n => [a<=0 => a=0]]
Axiom
11 ALL(a):ALL(b):[a e n & b e n => [a<=b <=> a<b | a=b]]
Axiom
12 ALL(a):ALL(b):[a e n & b e n => [a<=b => a<=b+1]]
Axiom
13 ALL(a):ALL(b):[a e n & b e n => [a<b+1 => a<=b]]
Axiom
PROOF
*****
Construct subset n' of n
Apply Subset Axiom
14 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [P(a)
& ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]]
Subset, 1
15 Set(n') & ALL(a):[a e n' <=> a e n & [P(a)
& ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
E Spec, 14
Define: n'
16 Set(n')
Split, 15
17 ALL(a):[a e n' <=> a e n & [P(a)
& ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
Split, 15
Apply the principle of ordinary induction
18 Set(n') & ALL(b):[b e n' => b e n]
=> [0 e n' & ALL(b):[b e n' => b+1 e n']
=> ALL(b):[b e n => b e n']]
U Spec, 7
Prove: ALL(b):[b e n' => b e n] i.e. n' is a subset of n
Suppose...
19 x e n'
Premise
Apply definition on n'
20 x e n' <=> x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
U Spec, 17
21 [x e n' => x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]]
& [x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]] => x e n']
Iff-And, 20
22 x e n' => x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
Split, 21
23 x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]] => x e n'
Split, 21
24 x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
Detach, 22, 19
25 x e n
Split, 24
As Required:
26 ALL(b):[b e n' => b e n]
4 Conclusion, 19
Joining results
27 Set(n') & ALL(b):[b e n' => b e n]
Join, 16, 26
Sufficient: For ALL(b):[b e n => b e n']
28 0 e n' & ALL(b):[b e n' => b+1 e n']
=> ALL(b):[b e n => b e n']
Detach, 18, 27
BASE CASE
*********
Prove: 0 e n'
Apply definition of n'
29 0 e n' <=> 0 e n & [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]]
U Spec, 17
30 [0 e n' => 0 e n & [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]]]
& [0 e n & [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]] => 0 e n']
Iff-And, 29
31 0 e n' => 0 e n & [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]]
Split, 30
Sufficient: For 0 e n'
32 0 e n & [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]] => 0 e n'
Split, 30
Prove: ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]
Suppose...
33 P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
Premise
34 P(0)
Split, 33
35 ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
Split, 33
Prove: ALL(b):[b e n => [b<=0 => P(b)]]
Suppose...
36 x e n
Premise
Prove: x<=0 => P(x)
Suppose...
37 x<=0
Premise
Apply property of <=
38 x e n => [x<=0 => x=0]
U Spec, 10
39 x<=0 => x=0
Detach, 38, 36
40 x=0
Detach, 39, 37
41 P(x)
Substitute, 40, 34
As Required:
42 x<=0 => P(x)
4 Conclusion, 37
As Required:
43 ALL(b):[b e n => [b<=0 => P(b)]]
4 Conclusion, 36
As Required:
44 P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]
4 Conclusion, 33
Joining results
45 0 e n
& [P(0)
& ALL(b):[b e n => [0<b & b<=0 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=0 => P(b)]]]
Join, 2, 44
Base case
As Required:
46 0 e n'
Detach, 32, 45
INDUCTIVE STEP
**************
Prove: ALL(b):[b e n' => b+1 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 => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
U Spec, 17
49 [x e n' => x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]]
& [x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> 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 => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
Split, 49
51 x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> 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 => [0<b & b<=x => [P(b) => P(b-1)]]]
=> 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 => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]
Split, 52
Apply defintion of n'
55 x+1 e n' <=> x+1 e n & [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]]
U Spec, 17
56 [x+1 e n' => x+1 e n & [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]]]
& [x+1 e n & [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]] => x+1 e n']
Iff-And, 55
57 x+1 e n' => x+1 e n & [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]]
Split, 56
Sufficient: For x+1 e n'
58 x+1 e n & [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]] => x+1 e n'
Split, 56
Apply defintion of +
59 ALL(b):[x e n & b e n => x+b e n]
U Spec, 4
60 x e n & 1 e n => x+1 e n
U Spec, 59
61 x e n & 1 e n
Join, 53, 3
As Required:
62 x+1 e n
Detach, 60, 61
Prove: P(x+1) & ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]
Suppose...
63 P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
Premise
64 P(x+1)
Split, 63
Prove: P(x)
Apply premise
65 ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
Split, 63
66 x+1 e n => [0<x+1 & x+1<=x+1 => [P(x+1) => P(x+1-1)]]
U Spec, 65
67 0<x+1 & x+1<=x+1 => [P(x+1) => P(x+1-1)]
Detach, 66, 62
Apply property of <
68 x e n => 0<x+1
U Spec, 6
69 0<x+1
Detach, 68, 53
Apply reflexivity of =
70 x+1=x+1
Reflex
Apply property of < and <=
71 ALL(b):[x+1 e n & b e n => [x+1<=b <=> x+1<b | x+1=b]]
U Spec, 11
72 x+1 e n & x+1 e n => [x+1<=x+1 <=> x+1<x+1 | x+1=x+1]
U Spec, 71
73 x+1 e n & x+1 e n
Join, 62, 62
74 x+1<=x+1 <=> x+1<x+1 | x+1=x+1
Detach, 72, 73
75 [x+1<=x+1 => x+1<x+1 | x+1=x+1]
& [x+1<x+1 | x+1=x+1 => x+1<=x+1]
Iff-And, 74
76 x+1<=x+1 => x+1<x+1 | x+1=x+1
Split, 75
77 x+1<x+1 | x+1=x+1 => x+1<=x+1
Split, 75
78 x+1<x+1 | x+1=x+1
Arb Or, 70
79 x+1<=x+1
Detach, 77, 78
80 0<x+1 & x+1<=x+1
Join, 69, 79
81 P(x+1) => P(x+1-1)
Detach, 67, 80
82 P(x+1-1)
Detach, 81, 64
Prove: x+1-1=x
Apply definition of -
83 ALL(b):ALL(c):[x+1 e n & b e n & c e n => [x+1-b=c <=> x+1=c+b]]
U Spec, 5
84 ALL(c):[x+1 e n & 1 e n & c e n => [x+1-1=c <=> x+1=c+1]]
U Spec, 83
85 x+1 e n & 1 e n & x e n => [x+1-1=x <=> x+1=x+1]
U Spec, 84
86 x+1 e n & 1 e n
Join, 62, 3
87 x+1 e n & 1 e n & x e n
Join, 86, 53
88 x+1-1=x <=> x+1=x+1
Detach, 85, 87
89 [x+1-1=x => x+1=x+1] & [x+1=x+1 => x+1-1=x]
Iff-And, 88
90 x+1-1=x => x+1=x+1
Split, 89
91 x+1=x+1 => x+1-1=x
Split, 89
As Required:
92 x+1-1=x
Detach, 91, 70
As Required:
93 P(x)
Substitute, 92, 82
Prove: ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
Suppose...
94 y e n
Premise
Prove: 0<y & y<=x => [P(y) => P(y-1)]
Suppose...
95 0<y & y<=x
Premise
96 0<y
Split, 95
97 y<=x
Split, 95
Prove: P(y) => P(y-1)
Apply premise
98 y e n => [0<y & y<=x+1 => [P(y) => P(y-1)]]
U Spec, 65
99 0<y & y<=x+1 => [P(y) => P(y-1)]
Detach, 98, 94
100 ALL(b):[y e n & b e n => [y<=b => y<=b+1]]
U Spec, 12
101 y e n & x e n => [y<=x => y<=x+1]
U Spec, 100
102 y e n & x e n
Join, 94, 53
103 y<=x => y<=x+1
Detach, 101, 102
104 y<=x+1
Detach, 103, 97
105 0<y & y<=x+1
Join, 96, 104
As Required:
106 P(y) => P(y-1)
Detach, 99, 105
As Required:
107 0<y & y<=x => [P(y) => P(y-1)]
4 Conclusion, 95
As Required:
108 ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
4 Conclusion, 94
109 P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
Join, 93, 108
As Required:
110 ALL(b):[b e n => [b<=x => P(b)]]
Detach, 54, 109
Prove: ALL(b):[b e n => [b<=x+1 => P(b)]]
Suppose...
111 y e n
Premise
Prove: y<=x+1 => P(y)
Suppose...
112 y<=x+1
Premise
Apply property of < and <=
113 ALL(b):[y e n & b e n => [y<=b <=> y<b | y=b]]
U Spec, 11
114 y e n & x+1 e n => [y<=x+1 <=> y<x+1 | y=x+1]
U Spec, 113
115 y e n & x+1 e n
Join, 111, 62
116 y<=x+1 <=> y<x+1 | y=x+1
Detach, 114, 115
117 [y<=x+1 => y<x+1 | y=x+1] & [y<x+1 | y=x+1 => y<=x+1]
Iff-And, 116
118 y<=x+1 => y<x+1 | y=x+1
Split, 117
119 y<x+1 | y=x+1 => y<=x+1
Split, 117
Two cases to consider:
120 y<x+1 | y=x+1
Detach, 118, 112
Case 1
Prove: y<x+1 => P(y)
Suppose...
121 y<x+1
Premise
Apply previous result
122 y e n => [y<=x => P(y)]
U Spec, 110
123 y<=x => P(y)
Detach, 122, 111
Apply property of <
124 ALL(b):[y e n & b e n => [y<b+1 => y<=b]]
U Spec, 13
125 y e n & x e n => [y<x+1 => y<=x]
U Spec, 124
126 y e n & x e n
Join, 111, 53
127 y<x+1 => y<=x
Detach, 125, 126
128 y<=x
Detach, 127, 121
As Required:
129 P(y)
Detach, 123, 128
Case 1
As Required:
130 y<x+1 => P(y)
4 Conclusion, 121
Case 2
Prove: y=x+1 => P(y)
Suppose...
131 y=x+1
Premise
132 P(y)
Substitute, 131, 64
Case 2
As Required:
133 y=x+1 => P(y)
4 Conclusion, 131
134 [y<x+1 => P(y)] & [y=x+1 => P(y)]
Join, 130, 133
135 P(y)
Cases, 120, 134
As Required:
136 y<=x+1 => P(y)
4 Conclusion, 112
As Required:
137 ALL(b):[b e n => [b<=x+1 => P(b)]]
4 Conclusion, 111
As Required:
138 P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]
4 Conclusion, 63
Joining results
139 x+1 e n
& [P(x+1)
& ALL(b):[b e n => [0<b & b<=x+1 => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x+1 => P(b)]]]
Join, 62, 138
140 x+1 e n'
Detach, 58, 139
Inductive step
As Required:
141 ALL(b):[b e n' => b+1 e n']
4 Conclusion, 47
GENERALIZING
************
Joining results
142 0 e n' & ALL(b):[b e n' => b+1 e n']
Join, 46, 141
As Required:
143 ALL(b):[b e n => b e n']
Detach, 28, 142
Prove: ALL(a):[a e n
=> [P(a) & ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
Suppose...
144 x e n
Premise
145 x e n => x e n'
U Spec, 143
146 x e n'
Detach, 145, 144
Apply definition of n'
147 x e n' <=> x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
U Spec, 17
148 [x e n' => x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]]
& [x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]] => x e n']
Iff-And, 147
149 x e n' => x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
Split, 148
150 x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]] => x e n'
Split, 148
151 x e n & [P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]]
Detach, 149, 146
152 x e n
Split, 151
153 P(x)
& ALL(b):[b e n => [0<b & b<=x => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=x => P(b)]]
Split, 151
As Required:
154 ALL(a):[a e n
=> [P(a)
& ALL(b):[b e n => [0<b & b<=a => [P(b) => P(b-1)]]]
=> ALL(b):[b e n => [b<=a => P(b)]]]]
4 Conclusion, 144