THEOREM

*******

 

Let s be a non-empty set with function f: s --> s. There exists a subset n of s and x0 e n such that the Induction Principle holds on n with x0 being the "first" element of n and f being the successor function.

 

COROLLARY

*********

 

Let x be a non-empty set. Then there exists a subset n of x, x0 e n and f: n --> n such that the Induction Principle holds on n with x0 being the "first" element of n and f being the successor function.

 

 

Lines

-----

 

7-10   Construct n using Subset Axiom

11-18  Prove n is a subset of s

19-29  Prove x0 e n

30-62  Prove f is closed on n

63-89  Prove induction principle holds on n

90-94  Generalize

95-111 Prove corollary

 

 

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

 

 

PREVIOUS RESULT

***************

 

Let s be a set. Then there exists a function f on s such that f(x)=x. Used for corollary.  PROOF

 

1     ALL(s):[Set(s) => EXIST(f):ALL(a):[a e s => f(a)=a]]

      Axiom

 

    

     PROOF OF THEOREM

     ****************

    

     Let s be a non-empty set with function f: s --> s

 

      2     Set(s) & EXIST(a):a e s & ALL(a):[a e s => f(a) e s]

            Premise

 

      3     Set(s)

            Split, 2

 

      4     EXIST(a):a e s

            Split, 2

 

      5     ALL(a):[a e s => f(a) e s]

            Split, 2

 

     Define: x0

 

      6     x0 e s

            E Spec, 4

 

     Construct set n

    

     Apply Subset Axiom

 

      7     EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Subset, 3

 

      8     Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            E Spec, 7

 

     Define: n

 

      9     Set(n)

            Split, 8

 

      10    ALL(a):[a e n <=> a e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Split, 8

 

         

          Prove: n is a subset of s

         

          Suppose...

 

            11    x e n

                  Premise

 

          Apply definition of n

 

            12    x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  U Spec, 10

 

            13    [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

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

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

                  Iff-And, 12

 

            14    x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 13

 

            15    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 13

 

            16    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Detach, 14, 11

 

            17    x e s

                  Split, 16

 

     As Required:

 

      18    ALL(a):[a e n => a e s]

            4 Conclusion, 11

 

    

     Prove that the set n has the required properties. Show that n = {x0, f(x0), f(f(x0)), ...}

    

     Prove: x0 e n

    

     Apply definition of n

 

      19    x0 e n <=> x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            U Spec, 10

 

      20    [x0 e n => x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

          & [x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Iff-And, 19

 

      21    x0 e n => x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Split, 20

 

     Sufficient: For x0 e n

 

      22    x0 e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Split, 20

 

         

          Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

         

          Suppose...

 

            23    Set(q) & ALL(c):[c e q => c e s]

                  Premise

 

             

              Prove: x0 e q & ALL(c):[c e q => f(c) e q] => x0 e q => x0 eq

             

              Suppose...

 

                  24    x0 e q & ALL(c):[c e q => f(c) e q]

                        Premise

 

                  25    x0 e q

                        Split, 24

 

          As Required:

 

            26    x0 e q & ALL(c):[c e q => f(c) e q] => x0 e q

                  4 Conclusion, 24

 

     As Required:

 

      27    ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            4 Conclusion, 23

 

      28    x0 e s

          & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

            Join, 6, 27

 

     As Required:

 

      29    x0 e n

            Detach, 22, 28

 

         

          Prove: f is closed on n

         

          Suppose...

 

            30    x e n

                  Premise

 

          Apply definition of n

 

            31    x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  U Spec, 10

 

            32    [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

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

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

                  Iff-And, 31

 

            33    x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 32

 

            34    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 32

 

            35    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Detach, 33, 30

 

            36    x e s

                  Split, 35

 

            37    ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 35

 

          Apply the definition of n

 

            38    f(x) e n <=> f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  U Spec, 10

 

            39    [f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

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

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

                  Iff-And, 38

 

            40    f(x) e n => f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 39

 

          Sufficient: For f(x) e n

 

            41    f(x) e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Split, 39

 

          Prove: f(x) e s

         

          Apply previous result

 

            42    x e n => x e s

                  U Spec, 18

 

            43    x e s

                  Detach, 42, 30

 

          Apply the definition of f

 

            44    x e s => f(x) e s

                  U Spec, 5

 

          As Required:

 

            45    f(x) e s

                  Detach, 44, 43

 

             

              Prove: ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

             

              Suppose...

 

                  46    Set(q) & ALL(c):[c e q => c e s]

                        Premise

 

                  47    Set(q)

                        Split, 46

 

                  48    ALL(c):[c e q => c e s]

                        Split, 46

 

                  

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

                  

                   Suppose...

 

                        49    x0 e q & ALL(c):[c e q => f(c) e q]

                              Premise

 

                        50    x0 e q

                              Split, 49

 

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

                              Split, 49

 

                   Sufficient: For f(x) e q

 

                        52    x e q => f(x) e q

                              U Spec, 51

 

                   Prove: x e q

                  

                   Apply previous result

 

                        53    Set(q) & ALL(c):[c e q => c e s]

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

                              U Spec, 37

 

                   Sufficient: For x e q

 

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

                              Detach, 53, 46

 

                        55    x0 e q & ALL(c):[c e q => f(c) e q]

                              Join, 50, 51

 

                   As Required:

 

                        56    x e q

                              Detach, 54, 55

 

                   As Required:

 

                        57    f(x) e q

                              Detach, 52, 56

 

              As Required:

 

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

                        4 Conclusion, 49

 

          As Required:

 

            59    ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  4 Conclusion, 46

 

            60    f(x) e s

              & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                  Join, 45, 59

 

          As Required:

 

            61    f(x) e n

                  Detach, 41, 60

 

     As Required:

 

      62    ALL(a):[a e n => f(a) e n]

            4 Conclusion, 30

 

          Induction Principle

          *******************

         

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

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

                 => ALL(c):[c e n => c e a]]]

         

          Suppose...

 

            63    Set(p) & ALL(b):[b e p => b e n]

                  Premise

 

            64    Set(p)

                  Split, 63

 

          p is a subset of n

 

            65    ALL(b):[b e p => b e n]

                  Split, 63

 

             

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

                     => ALL(c):[c e n => c e p]

             

              Suppose...

 

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

                        Premise

 

                  67    x0 e p

                        Split, 66

 

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

                        Split, 66

 

                  

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

                  

                   Suppose...

 

                        69    x e n

                              Premise

 

                   Apply definition of n

 

                        70    x e n <=> x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                              U Spec, 10

 

                        71    [x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

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

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

                              Iff-And, 70

 

                        72    x e n => x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                              Split, 71

 

                        73    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                              Split, 71

 

                        74    x e s & ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                              Detach, 72, 69

 

                        75    x e s

                              Split, 74

 

                        76    ALL(b):[Set(b) & ALL(c):[c e b => c e s]

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

                              Split, 74

 

                        77    Set(p) & ALL(c):[c e p => c e s]

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

                              U Spec, 76

 

                       

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

                       

                        Suppose...

 

                              78    y e p

                                    Premise

 

                        Apply definition of p

 

                              79    y e p => y e n

                                    U Spec, 65

 

                              80    y e n

                                    Detach, 79, 78

 

                        Apply previous result

 

                              81    y e n => y e s

                                    U Spec, 18

 

                              82    y e s

                                    Detach, 81, 80

 

                   As Required:

 

                        83    ALL(c):[c e p => c e s]

                              4 Conclusion, 78

 

                        84    Set(p) & ALL(c):[c e p => c e s]

                              Join, 64, 83

 

                        85    x0 e p & ALL(c):[c e p => f(c) e p] => x e p

                              Detach, 77, 84

 

                        86    x e p

                              Detach, 85, 66

 

              As Required:

 

                  87    ALL(c):[c e n => c e p]

                        4 Conclusion, 69

 

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

              => ALL(c):[c e n => c e p]

                  4 Conclusion, 66

 

     As Required:

 

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

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

          => ALL(c):[c e n => c e a]]]

            4 Conclusion, 63

 

      90    Set(n) & ALL(a):[a e n => a e s]

            Join, 9, 18

 

      91    Set(n) & ALL(a):[a e n => a e s] & x0 e n

            Join, 90, 29

 

      92    Set(n) & ALL(a):[a e n => a e s] & x0 e n

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

            Join, 91, 62

 

      93    Set(n) & ALL(a):[a e n => a e s] & x0 e n

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

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

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

          => ALL(c):[c e n => c e a]]]

            Join, 92, 89

 

 

As Required:

 

94    ALL(s):ALL(f):[Set(s) & EXIST(a):a e s & ALL(a):[a e s => f(a) e s]

     => EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e s] & x0 e n

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

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

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

     => ALL(c):[c e n => c e a]]]]]

      4 Conclusion, 2

 

    

     PROOF OF COROLLARY

     ******************

    

     Suppose...

 

      95    Set(x) & EXIST(a):a e x

            Premise

 

      96    Set(x)

            Split, 95

 

      97    EXIST(a):a e x

            Split, 95

 

     Define: x0

 

      98    x0 e x

            E Spec, 97

 

     Apply previous result

 

      99    Set(x) => EXIST(f):ALL(a):[a e x => f(a)=a]

            U Spec, 1

 

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

            Detach, 99, 96

 

     Define: f

 

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

            E Spec, 100

 

     Apply theorem

 

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

          => EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

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

          => ALL(c):[c e n => c e a]]]]]

            U Spec, 94

 

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

          => EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

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

          => ALL(c):[c e n => c e a]]]]

            U Spec, 102

 

         

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

         

          Suppose...

 

            104  y e x

                  Premise

 

            105  y e x => f(y)=y

                  U Spec, 101

 

            106  f(y)=y

                  Detach, 105, 104

 

            107  f(y) e x

                  Substitute, 106, 104

 

     As Required:

 

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

            4 Conclusion, 104

 

      109  Set(x) & EXIST(a):a e x

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

            Join, 95, 108

 

      110  EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

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

          => ALL(c):[c e n => c e a]]]]

            Detach, 103, 109

 

 

As Required:

 

111  ALL(x):[Set(x) & EXIST(a):a e x

     => EXIST(f):EXIST(n):EXIST(x0):[Set(n) & ALL(a):[a e n => a e x] & x0 e n

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

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

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

     => ALL(c):[c e n => c e a]]]]]

      4 Conclusion, 95