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

 

 

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

 

††††††††††††††††† 100f(y) e p' => f(y) e x & ~f(y) e p

††††††††††††††††††††††† Split, 99

 

††††††††††††††††† 101f(y) e x & ~f(y) e p => f(y) e p'

††††††††††††††††††††††† Split, 99

 

††††††††††††††††† 102f(y) e x & ~f(y) e p

††††††††††††††††††††††† Detach, 100, 85

 

††††††††††††††††† 103f(y) e x

††††††††††††††††††††††† Split, 102

 

††††††††††††††††† 104~f(y) e p

††††††††††††††††††††††† Split, 102

 

†††††††††††† Obtain the contradiction...

 

††††††††††††††††† 105f(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

 

††††† 109Accessible(x,f,x0) => ~~Induction(x,f,x0)

††††††††††† Rem DNeg, 108

 

††† As Required:

 

††††† 110Accessible(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)

 

††††††††††† 112ALL(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

 

††††††††††† 113ALL(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

 

††††††††††† 114Accessible(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

 

††††††††††† 116Accessible(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

 

††††††††††† 117ALL(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

 

††††††††††† 121EXIST(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

 

††††††††††† 122EXIST(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

 

††††††††††† 123EXIST(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

 

††††††††††† 124EXIST(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

 

††††††††††† 125EXIST(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

 

††††††††††† 126EXIST(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

 

††††††††††† 127EXIST(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

 

††††††††††† 128EXIST(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

 

††††††††††† 129EXIST(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

 

††††††††††† 130Set(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'

 

††††††††††† 131Set(p')

††††††††††††††††† Split, 130

 

††††††††††† 132ALL(c):[c e p' => c e x]

††††††††††††††††† Split, 130

 

††††††††††† 133EXIST(c):c e p'

††††††††††††††††† Split, 130

 

††††††††††† 134~x0 e p'

††††††††††††††††† Split, 130

 

††††††††††† 135ALL(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)

 

††††††††††† 136ALL(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

 

††††††††††† 137ALL(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

 

††††††††††† 138Induction(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

 

††††††††††† 140Induction(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

 

††††††††††† 141ALL(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

 

††††††††††† 144EXIST(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

 

††††††††††† 145EXIST(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

 

††††††††††† 146EXIST(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

 

††††††††††† 147EXIST(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

 

††††††††††† 148EXIST(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

 

††††††††††† 149EXIST(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

 

††††††††††† 150EXIST(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

 

††††††††††† 151EXIST(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)

 

††††††††††† 152EXIST(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

 

††††††††††† 153EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & ~a e p']]

††††††††††††††††† Subset, 4

 

††††††††††† 154Set(p) & ALL(a):[a e p <=> a e x & ~a e p']

††††††††††††††††† E Spec, 153

 

††††††††

†††††††† Define: p

 

††††††††††† 155Set(p)

††††††††††††††††† Split, 154

 

††††††††††† 156ALL(a):[a e p <=> a e x & ~a e p']

††††††††††††††††† Split, 154

 

††††††††††††

†††††††††††† Prove: ALL(c):[c e p => c e x]

††††††††††††

†††††††††††† Suppose...

 

††††††††††††††††† 157t e p

††††††††††††††††††††††† Premise

 

††††††††††††††††† 158t 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

 

††††††††††††††††† 160t e p => t e x & ~t e p'

††††††††††††††††††††††† Split, 159

 

††††††††††††††††† 161t e x & ~t e p' => t e p

††††††††††††††††††††††† Split, 159

 

††††††††††††††††† 162t e x & ~t e p'

††††††††††††††††††††††† Detach, 160, 157

 

††††††††††††††††† 163t e x

††††††††††††††††††††††† Split, 162

 

†††††††† As Required:

 

††††††††††† 164ALL(c):[c e p => c e x]

††††††††††††††††† 4 Conclusion, 157

 

††††††††††† 165x0 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

 

††††††††††† 167x0 e p => x0 e x & ~x0 e p'

††††††††††††††††† Split, 166

 

††††††††††† 168x0 e x & ~x0 e p' => x0 e p

††††††††††††††††† Split, 166

 

††††††††††† 169x0 e x & ~x0 e p'

††††††††††††††††† Join, 5, 134

 

†††††††† As Required:

 

††††††††††† 170x0 e p

††††††††††††††††† Detach, 168, 169

 

††††††††††††

†††††††††††† Prove: ALL(c):[c e p => f(c) e p]

††††††††††††

†††††††††††† Suppose...

 

††††††††††††††††† 171t e p

††††††††††††††††††††††† Premise

 

††††††††††††††††† 172t 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

 

††††††††††††††††† 174t e p => t e x & ~t e p'

††††††††††††††††††††††† Split, 173

 

††††††††††††††††† 175t e x & ~t e p' => t e p

††††††††††††††††††††††† Split, 173

 

††††††††††††††††† 176t e x & ~t e p'

††††††††††††††††††††††† Detach, 174, 171

 

††††††††††††††††† 177t e x

††††††††††††††††††††††† Split, 176

 

††††††††††††††††† 178~t e p'

††††††††††††††††††††††† Split, 176

 

††††††††††††††††† 179t 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

 

††††††††††††††††† 182f(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

 

††††††††††††††††† 184f(t) e p => f(t) e x & ~f(t) e p'

††††††††††††††††††††††† Split, 183

 

††††††††††††††††† 185f(t) e x & ~f(t) e p' => f(t) e p

††††††††††††††††††††††† Split, 183

 

††††††††††††††††† 186t e x => f(t) e x

††††††††††††††††††††††† U Spec, 6

 

††††††††††††††††† 187f(t) e x

††††††††††††††††††††††† Detach, 186, 177

 

††††††††††††††††† 188f(t) e x & ~f(t) e p'

††††††††††††††††††††††† Join, 187, 181

 

††††††††††††††††† 189f(t) e p

††††††††††† ††††††††††† Detach, 185, 188

 

†††††††† As Required:

 

††††††††††† 190ALL(c):[c e p => f(c) e p]

††††††††††††††††† 4 Conclusion, 171

 

†††††††† Define: y0

 

††††††††††† 191y0 e p'

††††††††††††††††† E Spec, 133

 

††††††††††† 192y0 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

 

††††††††††† 194y0 e p => y0 e x & ~y0 e p'

††††††††††††††††† Split, 193

 

††††††††††† 195y0 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

 

††††††††††† 202y0 e p' => y0 e x

††††††††††††††††† U Spec, 132

 

††††††††††† 203y0 e x

††††††††††††††††† Detach, 202, 191

 

††††††††††† 204y0 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

 

††††††††††† 206y0 e p => y0 e x & ~y0 e p'

††††††††††††††††† Split, 205

 

††††††††††† 207y0 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

 

††††††††††† 214y0 e x & ~y0 e p

††††††††††††††††† Join, 203, 213

 

As required:

 

††††††††††† 215EXIST(c):[c e x & ~c e p]

††††††††††††††††† E Gen, 214

 

††††††††††† 216Set(p) & ALL(c):[c e p => c e x]

††††††††††††††††† Join, 155, 164

 

††††††††††† 217x0 e p & ALL(c):[c e p => f(c) e p]

††††††††††††††††† Join, 170, 190

 

††††††††††† 218x0 e p & ALL(c):[c e p => f(c) e p]

†††††††††††† & EXIST(c):[c e x & ~c e p]

††††††††††††††††† Join, 217, 215

 

††††††††††† 219Set(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

 

††††††††††† 220EXIST(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

 

††††† 224Induction(x,f,x0) => ~~Accessible(x,f,x0)

††††††††††† Rem DNeg, 223

 

††† As Required:

 

††††† 225Induction(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

 

††††† 227Induction(x,f,x0) <=> Accessible(x,f,x0)

††††††††††† Iff-And, 226

 

As Required:

 

228ALL(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