THEOREM
*******
ALL(x):ALL(x0):ALL(f):[Set(x)
& x0 e x
& ALL(a):[a e x => f(a) e x]
=>
[Induction(x,f,x0) <=> Accessible(x,f,x0)]]
This machine-verified formal proof was written with the aid of
the author’s DC Proof 2.0 software available at http://www.dcproof.com
BACKGROUND
**********
In the set of natural numbers N, any number is “accessible” from
0 by repeatedly going from one number to the next, starting at 0. In other
words, there are no elements of N that are “isolated” from 0 under the
successor function S. As I will attempt to show here, this self-evident property
turns out to be logically equivalent to the usual Principle of Mathematical
Induction.
Here we generalize the notions of induction and accessability
for any set x, function f: x --> x (the “successor” function) and x0 e x (the “first” element) and prove that induction will hold on (x,f,x0)
if and only if accessibility holds there.
We say that accessibility holds on (x,f,x0) if and only there exists
no subset of x that are “isolated” from x0 under the “successor” function f.
DEFINITIONS
***********
Define: Induction(a,f,a0)
(means induction holds on (a,f,a0))
1 ALL(a):ALL(f):ALL(a0):[Induction(a,f,a0)
<=> ALL(b):[Set(b)
& ALL(c):[c e b => c e a]
=> [a0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e a => c e b]]]]
Axiom
Define: Accessible(a,f,a0)
(means accessibility holds on (a,f,a0))
2 ALL(a):ALL(f):ALL(a0):[Accessible(a,f,a0)
<=> ALL(b):[Set(b)
& ALL(c):[c e b => c e a]
& EXIST(c):c e b
& ~a0 e b
=> EXIST(c):[c e a & [~c e b & f(c) e b]]]]
Axiom
PROOF
*****
Prove:
ALL(x):ALL(x0):ALL(f):[Set(x)
& x0 e x
& ALL(a):[a e x => f(a) e x]
=> [Induction(x,f,x0) <=> Accessible(x,f,x0)]]
Suppose...
3 Set(x)
& x0 e x
& ALL(a):[a e x => f(a) e x]
Premise
4 Set(x)
Split, 3
5 x0 e x
Split, 3
6 ALL(a):[a e x => f(a) e x]
Split, 3
Prove:
~Induction(x,f,x0) => ~Accessible(x,f,x0)
Suppose...
7 ~Induction(x,f,x0)
Premise
Apply the
definition of Induction(x,f,x0)
8 ALL(f):ALL(a0):[Induction(x,f,a0)
<=>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [a0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
U Spec, 1
9 ALL(a0):[Induction(x,f,a0)
<=>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [a0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
U Spec, 8
10 Induction(x,f,x0)
<=>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
U Spec, 9
11 [Induction(x,f,x0) =>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
&
[ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => Induction(x,f,x0)]
Iff-And, 10
12 Induction(x,f,x0) => ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Split, 11
13 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => Induction(x,f,x0)
Split, 11
14 ~Induction(x,f,x0) =>
~ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Contra, 13
15 ~ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Detach, 14, 7
16 ~~EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Quant, 15
17 EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Rem DNeg, 16
18 EXIST(b):~~[Set(b)
& ALL(c):[c e b => c e x] & ~[x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Imply-And, 17
19 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & ~[x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Rem DNeg, 18
20 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & ~~[x0 e b & ALL(c):[c e b => f(c) e b] & ~ALL(c):[c e x => c e b]]]
Imply-And, 19
21 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & ~ALL(c):[c e x => c e b]]]
Rem DNeg, 20
22 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & ~~EXIST(c):~[c e x => c e b]]]
Quant, 21
23 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):~[c e x => c e b]]]
Rem DNeg, 22
24 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):~~[c e x & ~c e b]]]
Imply-And, 23
25 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):[c e x & ~c e b]]]
Rem DNeg, 24
26 Set(p) &
ALL(c):[c e p => c e x] & [x0 e p & ALL(c):[c e p => f(c) e p] & EXIST(c):[c e x & ~c e p]]
E Spec, 25
Define: p
27 Set(p)
Split, 26
28 ALL(c):[c e p => c e x]
Split, 26
29 x0 e p & ALL(c):[c e p => f(c) e p] & EXIST(c):[c e x & ~c e p]
Split, 26
30 x0 e p
Split, 29
31 ALL(c):[c e p => f(c) e p]
Split, 29
32 EXIST(c):[c e x & ~c e p]
Split, 29
Define: y0
33 y0 e x & ~y0 e p
E Spec, 32
34 y0 e x
Split, 33
35 ~y0 e p
Split, 33
Prove:
~Accessible(x,f,x0)
Suppose to the
contrary...
36 Accessible(x,f,x0)
Premise
Apply the
definition of Accessible(x,f,x0)
37 ALL(f):ALL(a0):[Accessible(x,f,a0)
<=>
ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~a0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
U Spec, 2
38 ALL(a0):[Accessible(x,f,a0)
<=>
ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~a0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
U Spec, 37
39 Accessible(x,f,x0)
<=>
ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
U Spec, 38
40 [Accessible(x,f,x0) =>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
&
[ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]] => Accessible(x,f,x0)]
Iff-And, 39
41 Accessible(x,f,x0) =>
ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Split, 40
42 ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]] =>
Accessible(x,f,x0)
Split, 40
43 ALL(b):[Set(b)
&
ALL(c):[c e b => c e x]
&
EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Detach, 41, 36
44 EXIST(sub):[Set(sub)
& ALL(a):[a e sub <=> a e x & ~a e p]]
Subset, 4
45 Set(p') &
ALL(a):[a e p' <=> a e x & ~a e p]
E Spec, 44
Define: p'
46 Set(p')
Split, 45
47 ALL(a):[a e p' <=> a e x & ~a e p]
Split, 45
Prove:
ALL(b):[b e p' => b e x]
Suppose...
48 t e p'
Premise
49 t e p' <=> t e x & ~t e p
U Spec, 47
50 [t e p' => t e x & ~t e p] & [t e x & ~t e p => t e p']
Iff-And, 49
51 t e p' => t e x & ~t e p
Split, 50
52 t e x & ~t e p => t e p'
Split, 50
53 t e x & ~t e p
Detach, 51, 48
54 t e x
Split, 53
As Required:
55 ALL(b):[b e p' => b e x]
4 Conclusion, 48
56 y0 e p' <=> y0 e x & ~y0 e p
U Spec, 47
57 [y0 e p' => y0 e x & ~y0 e p]
& [y0 e x & ~y0 e p => y0 e p']
Iff-And, 56
58 y0 e p' => y0 e x & ~y0 e p
Split, 57
59 y0 e x & ~y0 e p => y0 e p'
Split, 57
60 y0 e p' <=> y0 e x & ~y0 e p
U Spec, 47
61 [y0 e p' => y0 e x & ~y0 e p]
& [y0 e x & ~y0 e p => y0 e p']
Iff-And, 60
62 y0 e p' => y0 e x & ~y0 e p
Split, 61
63 y0 e x & ~y0 e p => y0 e p'
Split, 61
64 y0 e p'
Detach, 63, 33
As Required:
65 EXIST(b):b e p'
E Gen, 64
66 x0 e p' <=> x0 e x & ~x0 e p
U Spec, 47
67 [x0 e p' => x0 e x & ~x0 e p]
& [x0 e x & ~x0 e p => x0 e p']
Iff-And, 66
68 x0 e p' => x0 e x & ~x0 e p
Split, 67
69 x0 e x & ~x0 e p => x0 e p'
Split, 67
70 ~[x0 e x & ~x0 e p] => ~x0 e p'
Contra, 68
71 ~~[~x0 e x | ~~x0 e p] => ~x0 e p'
DeMorgan, 70
72 ~x0 e x | ~~x0 e p => ~x0 e p'
Rem DNeg, 71
73 ~x0 e x | x0 e p => ~x0 e p'
Rem DNeg, 72
74 ~x0 e x | x0 e p
Arb Or, 30
As Required:
75 ~x0 e p'
Detach, 73, 74
76 Set(p')
&
ALL(c):[c e p' => c e x]
&
EXIST(c):c e p'
& ~x0 e p'
=>
EXIST(c):[c e x & [~c e p' & f(c) e p']]
U Spec, 43
77 Set(p') &
ALL(b):[b e p' => b e x]
Join, 46, 55
78 Set(p') &
ALL(b):[b e p' => b e x]
&
EXIST(b):b e p'
Join, 77, 65
79 Set(p') &
ALL(b):[b e p' => b e x]
&
EXIST(b):b e p'
& ~x0 e p'
Join, 78, 75
80 EXIST(c):[c e x & [~c e p' & f(c) e p']]
Detach, 76, 79
Define: y
81 y e x & [~y e p' & f(y) e p']
E Spec, 80
82 y e x
Split, 81
83 ~y e p' & f(y) e p'
Split, 81
84 ~y e p'
Split, 83
85 f(y) e p'
Split, 83
86 y e p' <=> y e x & ~y e p
U Spec, 47
87 [y e p' => y e x & ~y e p] & [y e x & ~y e p => y e p']
Iff-And, 86
88 y e p' => y e x & ~y e p
Split, 87
89 y e x & ~y e p => y e p'
Split, 87
90 ~y e p' => ~[y e x & ~y e p]
Contra, 89
91 ~[y e x & ~y e p]
Detach, 90, 84
92 ~~[y e x => ~~y e p]
Imply-And, 91
93 y e x => ~~y e p
Rem DNeg, 92
94 y e x => y e p
Rem DNeg, 93
95 y e p
Detach, 94, 82
96 y e p => f(y) e p
U Spec, 31
97 f(y) e p
Detach, 96, 95
98 f(y) e p' <=> f(y) e x & ~f(y) e p
U Spec, 47
99 [f(y) e p' => f(y) e x & ~f(y) e p]
& [f(y) e x & ~f(y) e p => f(y) e p']
Iff-And, 98
100 f(y) e p' => f(y) e x & ~f(y) e p
Split, 99
101 f(y) e x & ~f(y) e p => f(y) e p'
Split, 99
102 f(y) e x & ~f(y) e p
Detach, 100, 85
103 f(y) e x
Split, 102
104 ~f(y) e p
Split, 102
Obtain the
contradiction...
105 f(y) e p & ~f(y) e p
Join, 97, 104
106 ~Accessible(x,f,x0)
4 Conclusion, 36
As Required:
107 ~Induction(x,f,x0) =>
~Accessible(x,f,x0)
4 Conclusion, 7
108 ~~Accessible(x,f,x0) =>
~~Induction(x,f,x0)
Contra, 107
109 Accessible(x,f,x0) => ~~Induction(x,f,x0)
Rem DNeg, 108
As Required:
110 Accessible(x,f,x0) =>
Induction(x,f,x0)
Rem DNeg, 109
Prove:
~Accessible(x,f,x0) => ~Induction(x,f,x0)
Suppose...
111 ~Accessible(x,f,x0)
Premise
Apply the
definition of Induction(x,f,x0)
112 ALL(f):ALL(a0):[Accessible(x,f,a0)
<=>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~a0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
U Spec, 2
113 ALL(a0):[Accessible(x,f,a0)
<=>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~a0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
U Spec, 112
114 Accessible(x,f,x0)
<=>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
U Spec, 113
115 [Accessible(x,f,x0) =>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]]
& [ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]] =>
Accessible(x,f,x0)]
Iff-And, 114
116 Accessible(x,f,x0) =>
ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Split, 115
117 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]] =>
Accessible(x,f,x0)
Split, 115
118 ~Accessible(x,f,x0) => ~ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Contra, 117
119 ~ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Detach, 118, 111
120 ~~EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Quant, 119
121 EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b
=>
EXIST(c):[c e x & [~c e b & f(c) e b]]]
Rem DNeg, 120
122 EXIST(b):~~[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ~EXIST(c):[c e x & [~c e b & f(c) e b]]]
Imply-And, 121
123 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ~EXIST(c):[c e x & [~c e b & f(c) e b]]]
Rem DNeg, 122
124 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ~~ALL(c):~[c e x & [~c e b & f(c) e b]]]
Quant, 123
125 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ALL(c):~[c e x & [~c e b & f(c) e b]]]
Rem DNeg, 124
126 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ALL(c):~~[c e x => ~[~c e b & f(c) e b]]]
Imply-And, 125
127 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ALL(c):[c e x => ~[~c e b & f(c) e b]]]
Rem DNeg, 126
128 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ALL(c):[c e x => ~~[~c e b => ~f(c) e b]]]
Imply-And, 127
129 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& EXIST(c):c e b
& ~x0 e b & ALL(c):[c e x => [~c e b => ~f(c) e b]]]
Rem DNeg, 128
130 Set(p')
& ALL(c):[c e p' => c e x]
& EXIST(c):c e p'
& ~x0 e p' & ALL(c):[c e x => [~c e p' => ~f(c) e p']]
E Spec, 129
Define: p'
131 Set(p')
Split, 130
132 ALL(c):[c e p' => c e x]
Split, 130
133 EXIST(c):c e p'
Split, 130
134 ~x0 e p'
Split, 130
135 ALL(c):[c e x => [~c e p' => ~f(c) e p']]
Split, 130
Prove:
~Accessible(x,f,x0) => ~Induction(x,f,x0)
Apply the
definition of Induction(x,f,x0)
136 ALL(f):ALL(a0):[Induction(x,f,a0)
<=>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [a0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
U Spec, 1
137 ALL(a0):[Induction(x,f,a0)
<=> ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [a0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
U Spec, 136
138 Induction(x,f,x0)
<=>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
U Spec, 137
139 [Induction(x,f,x0) =>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]]
&
[ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => Induction(x,f,x0)]
Iff-And, 138
140 Induction(x,f,x0) =>
ALL(b):[Set(b) & ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]]
Split, 139
141 ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => Induction(x,f,x0)
Split, 139
142 ~ALL(b):[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Contra, 140
143 ~~EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Quant, 142
144 EXIST(b):~[Set(b)
& ALL(c):[c e b => c e x]
=> [x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Rem DNeg, 143
145 EXIST(b):~~[Set(b)
& ALL(c):[c e b => c e x] & ~[x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Imply-And, 144
146 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & ~[x0 e b & ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Rem DNeg, 145
147 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & ~~[x0 e b & ALL(c):[c e b => f(c) e b] & ~ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Imply-And, 146
148 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & ~ALL(c):[c e x => c e b]]] => ~Induction(x,f,x0)
Rem DNeg, 147
149 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & ~~EXIST(c):~[c e x => c e b]]] => ~Induction(x,f,x0)
Quant, 148
150 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):~[c e x => c e b]]] => ~Induction(x,f,x0)
Rem DNeg, 149
151 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):~~[c e x & ~c e b]]] => ~Induction(x,f,x0)
Imply-And, 150
Sufficient: For
~Induction(x,f,x0)
152 EXIST(b):[Set(b) & ALL(c):[c e b => c e x] & [x0 e b & ALL(c):[c e b => f(c) e b] & EXIST(c):[c e x & ~c e b]]] => ~Induction(x,f,x0)
Rem DNeg, 151
153 EXIST(sub):[Set(sub)
& ALL(a):[a e sub <=> a e x & ~a e p']]
Subset, 4
154 Set(p) &
ALL(a):[a e p <=> a e x & ~a e p']
E Spec, 153
Define: p
155 Set(p)
Split, 154
156 ALL(a):[a e p <=> a e x & ~a e p']
Split, 154
Prove:
ALL(c):[c e p => c e x]
Suppose...
157 t e p
Premise
158 t e p <=> t e x & ~t e p'
U Spec, 156
159 [t e p => t e x & ~t e p'] & [t e x & ~t e p' => t e p]
Iff-And, 158
160 t e p => t e x & ~t e p'
Split, 159
161 t e x & ~t e p' => t e p
Split, 159
162 t e x & ~t e p'
Detach, 160, 157
163 t e x
Split, 162
As Required:
164 ALL(c):[c e p => c e x]
4 Conclusion, 157
165 x0 e p <=> x0 e x & ~x0 e p'
U Spec, 156
166 [x0 e p => x0 e x & ~x0 e p']
& [x0 e x & ~x0 e p' => x0 e p]
Iff-And, 165
167 x0 e p => x0 e x & ~x0 e p'
Split, 166
168 x0 e x & ~x0 e p' => x0 e p
Split, 166
169 x0 e x & ~x0 e p'
Join, 5, 134
As Required:
170 x0 e p
Detach, 168, 169
Prove:
ALL(c):[c e p => f(c) e p]
Suppose...
171 t e p
Premise
172 t e p <=> t e x & ~t e p'
U Spec, 156
173 [t e p => t e x & ~t e p'] & [t e x & ~t e p' => t e p]
Iff-And, 172
174 t e p => t e x & ~t e p'
Split, 173
175 t e x & ~t e p' => t e p
Split, 173
176 t e x & ~t e p'
Detach, 174, 171
177 t e x
Split, 176
178 ~t e p'
Split, 176
179 t e x => [~t e p' => ~f(t) e p']
U Spec, 135
180 ~t e p' => ~f(t) e p'
Detach, 179, 177
181 ~f(t) e p'
Detach, 180, 178
182 f(t) e p <=> f(t) e x & ~f(t) e p'
U Spec, 156
183 [f(t) e p => f(t) e x & ~f(t) e p']
& [f(t) e x & ~f(t) e p' => f(t) e p]
Iff-And, 182
184 f(t) e p => f(t) e x & ~f(t) e p'
Split, 183
185 f(t) e x & ~f(t) e p' => f(t) e p
Split, 183
186 t e x => f(t) e x
U Spec, 6
187 f(t) e x
Detach, 186, 177
188 f(t) e x & ~f(t) e p'
Join, 187, 181
189 f(t) e p
Detach, 185, 188
As Required:
190 ALL(c):[c e p => f(c) e p]
4 Conclusion, 171
Define: y0
191 y0 e p'
E Spec, 133
192 y0 e p <=> y0 e x & ~y0 e p'
U Spec, 156
193 [y0 e p => y0 e x & ~y0 e p']
& [y0 e x & ~y0 e p' => y0 e p]
Iff-And, 192
194 y0 e p => y0 e x & ~y0 e p'
Split, 193
195 y0 e x & ~y0 e p' => y0 e p
Split, 193
196 ~[y0 e x & ~y0 e p'] => ~y0 e p
Contra, 194
197 ~~[~y0 e x | ~~y0 e p'] => ~y0 e p
DeMorgan, 196
198 ~y0 e x | ~~y0 e p' => ~y0 e p
Rem DNeg, 197
199 ~y0 e x | y0 e p' => ~y0 e p
Rem DNeg, 198
200 ~y0 e x | y0 e p'
Arb Or, 191
As Required:
201 ~y0 e p
Detach, 199, 200
202 y0 e p' => y0 e x
U Spec, 132
203 y0 e x
Detach, 202, 191
204 y0 e p <=> y0 e x & ~y0 e p'
U Spec, 156
205 [y0 e p => y0 e x & ~y0 e p']
& [y0 e x & ~y0 e p' => y0 e p]
Iff-And, 204
206 y0 e p => y0 e x & ~y0 e p'
Split, 205
207 y0 e x & ~y0 e p' => y0 e p
Split, 205
208 ~[y0 e x & ~y0 e p'] => ~y0 e p
Contra, 206
209 ~~[~y0 e x | ~~y0 e p'] => ~y0 e p
DeMorgan, 208
210 ~y0 e x | ~~y0 e p' => ~y0 e p
Rem DNeg, 209
211 ~y0 e x | y0 e p' => ~y0 e p
Rem DNeg, 210
212 ~y0 e x | y0 e p'
Arb Or, 191
213 ~y0 e p
Detach, 211, 212
214 y0 e x & ~y0 e p
Join, 203, 213
As required:
215 EXIST(c):[c e x & ~c e p]
E Gen, 214
216 Set(p) &
ALL(c):[c e p => c e x]
Join, 155, 164
217 x0 e p & ALL(c):[c e p => f(c) e p]
Join, 170, 190
218 x0 e p & ALL(c):[c e p => f(c) e p]
&
EXIST(c):[c e x & ~c e p]
Join, 217, 215
219 Set(p) &
ALL(c):[c e p => c e x]
& [x0 e p & ALL(c):[c e p => f(c) e p]
&
EXIST(c):[c e x & ~c e p]]
Join, 216, 218
220 EXIST(b):[Set(b)
& ALL(c):[c e b => c e x]
& [x0 e b & ALL(c):[c e b => f(c) e b]
&
EXIST(c):[c e x & ~c e b]]]
E Gen, 219
221 ~Induction(x,f,x0)
Detach, 152, 220
As Required:
222 ~Accessible(x,f,x0) => ~Induction(x,f,x0)
4 Conclusion, 111
223 ~~Induction(x,f,x0) =>
~~Accessible(x,f,x0)
Contra, 222
224 Induction(x,f,x0) =>
~~Accessible(x,f,x0)
Rem DNeg, 223
As Required:
225 Induction(x,f,x0) =>
Accessible(x,f,x0)
Rem DNeg, 224
226 [Induction(x,f,x0) =>
Accessible(x,f,x0)]
& [Accessible(x,f,x0) =>
Induction(x,f,x0)]
Join, 225, 110
227 Induction(x,f,x0) <=>
Accessible(x,f,x0)
Iff-And, 226
As Required:
228 ALL(x):ALL(x0):ALL(f):[Set(x)
& x0 e x
& ALL(a):[a e x => f(a) e x]
=> [Induction(x,f,x0)
<=> Accessible(x,f,x0)]]
4 Conclusion, 3