THEOREM

*******

For any (possibly finite) set x, x0ex and f: x --> x such that x = {x0, f(x0), f(f(x0)), ... }, induction will hold on x with "first" number x0 and successor function f.

Note that x here is just the smallest set containing x0, f(x0), f(f(x0)), ... i.e. every element of x can be reached by a process of repeated application of function f starting at x0.

Prove: ALL(x):ALL(x0):ALL(f):[Set(x)

& x0 e x

& ALL(a):[a e x => f(a) e x]

& ALL(a):[a e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]

=> ALL(a):[Set(a) & ALL(b):[b e a => b e x] <--- Induction holds on x

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e x => b e a]]]]

This machine-verified formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

PROOF

*****

Suppose...

1 Set(x)

& x0 e x

& ALL(a):[a e x => f(a) e x]

& ALL(a):[a e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]

Premise

x is a set

2 Set(x)

Split, 1

3 x0 e x

Split, 1

Define: f (a function mapping x to itself)

4 ALL(a):[a e x => f(a) e x]

Split, 1

Define: x (the smallest set that contains x0, f(x0), f(f(x0)), ... )

5 ALL(a):[a e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]

Split, 1

Prove: ALL(a):[a e x => f(a) e x]

Suppose...

6 t e x

Premise

Apply definition of x for a=t

7 t e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]

U Spec, 5

8 [t e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t 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] => t e b] => t e x]

Iff-And, 7

9 t e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]

Split, 8

10 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b] => t e x

Split, 8

11 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => t e b]

Detach, 9, 6

Apply the definition of x for a=f(t)

12 f(t) e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b]

U Spec, 5

13 [f(t) e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) 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] => f(t) e b] => f(t) e x]

Iff-And, 12

14 f(t) e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => f(t) e b]

Split, 13

Sufficient: For f(t) e x

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] => f(t) e b] => f(t) e x

Split, 13

Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]

=> f(t) e b]

Suppose...

16 Set(q) & ALL(c):[c e q => c e x] & x0 e q & ALL(c):[c e q => f(c) e q]

Premise

17 Set(q)

Split, 16

18 ALL(c):[c e q => c e x]

Split, 16

19 x0 e q

Split, 16

20 ALL(c):[c e q => f(c) e q]

Split, 16

Apply previous result

21 Set(q) & ALL(c):[c e q => c e x] & x0 e q & ALL(c):[c e q => f(c) e q] => t e q

U Spec, 11

22 t e q

Detach, 21, 16

Apply previous result

23 t e q => f(t) e q

U Spec, 20

24 f(t) e q

Detach, 23, 22

As Required:

25 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b]

=> f(t) e b]

4 Conclusion, 16

26 f(t) e x

Detach, 15, 25

As Required:

27 ALL(a):[a e x => f(a) e x]

4 Conclusion, 6

Prove: Induction holds on x with "first" element x0 and successor function f

Suppose p is a subset of x

28 Set(p) & ALL(b):[b e p => b e x]

Premise

Prove: x0 e p & ALL(b):[b e p => f(b) e p]

=> ALL(b):[b e x => b e p]

Suppose...

29 x0 e p & ALL(b):[b e p => f(b) e p]

Premise

30 x0 e p

Split, 29

31 ALL(b):[b e p => f(b) e p]

Split, 29

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

Suppose...

32 u e x

Premise

Apply the definition of x for a=u

33 u e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => u e b]

U Spec, 5

34 [u e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => u 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] => u e b] => u e x]

Iff-And, 33

35 u e x => ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => u e b]

Split, 34

36 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => u e b] => u e x

Split, 34

37 ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => u e b]

Detach, 35, 32

38 Set(p) & ALL(c):[c e p => c e x] & x0 e p & ALL(c):[c e p => f(c) e p] => u e p

U Spec, 37

39 Set(p) & ALL(b):[b e p => b e x] & x0 e p

Join, 28, 30

40 Set(p) & ALL(b):[b e p => b e x] & x0 e p

& ALL(b):[b e p => f(b) e p]

Join, 39, 31

41 u e p

Detach, 38, 40

As Required:

42 ALL(b):[b e x => b e p]

4 Conclusion, 32

As Required:

43 x0 e p & ALL(b):[b e p => f(b) e p]

=> ALL(b):[b e x => b e p]

4 Conclusion, 29

Induction holds on x with "first" element x0 and successor function f

As Required:

44 ALL(a):[Set(a) & ALL(b):[b e a => b e x]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e x => b e a]]]

4 Conclusion, 28

As Required:

45 ALL(x):ALL(x0):ALL(f):[Set(x)

& x0 e x

& ALL(a):[a e x => f(a) e x]

& ALL(a):[a e x <=> ALL(b):[Set(b) & ALL(c):[c e b => c e x] & x0 e b & ALL(c):[c e b => f(c) e b] => a e b]]

=> ALL(a):[Set(a) & ALL(b):[b e a => b e x]

=> [x0 e a & ALL(b):[b e a => f(b) e a]

=> ALL(b):[b e x => b e a]]]]

4 Conclusion, 1