THEOREM

*******

 

For any set s with element s1 e s and f: s --> s there exists n such that:

 

  - n is a subset of s

  - s1 e n

  - f is closed on n

  - the induction principle is applicable on n with successor function f

 

Informally: n = {s1, f(s1), f(f(s1), ...}

 

 

OUTLINE OF PROOF

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

 

Lines

-----

5-8   Construct n using Subset Axiom

9-19  Prove s1 e n                  

20-47 Prove ALL(a):[aen => f(a) e n]

48-55 Prove n is a subset of s

56-88 Prove induction principle holds on n using successor function f

 

 

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

 

    

     Prove: ALL(s):ALL(s1):ALL(f):[Set(s)

            & s1 e s

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

            => EXIST(n):[Set(n)

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

            & s1 e n

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

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

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

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

    

     Suppose...

 

      1     Set(s)

          & s1 e s

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

            Premise

 

     Splitting premise...

 

      2     Set(s)

            Split, 1

 

      3     s1 e s

            Split, 1

 

     f is a function mapping s to itself

 

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

            Split, 1

 

     Construct n

    

     Apply Subset Axiom

 

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

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

            Subset, 2

 

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

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

            E Spec, 5

 

     Define: n

 

      7     Set(n)

            Split, 6

 

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

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

            Split, 6

 

     Prove: s1 e n

    

     Apply definition of n

 

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

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

            U Spec, 8

 

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

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

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

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

            Iff-And, 9

 

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

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

            Split, 10

 

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

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

            Split, 10

 

         

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

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

         

          Suppose...

 

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

                  Premise

 

             

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

             

              Suppose...

 

                  14    s1 e q & ALL(c):[c e q => f(c) e q]

                        Premise

 

                  15    s1 e q

                        Split, 14

 

          As Required:

 

            16    s1 e q & ALL(c):[c e q => f(c) e q] => s1 e q

                  4 Conclusion, 14

 

     As Required:

 

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

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

            4 Conclusion, 13

 

     Joining results...

 

      18    s1 e s

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

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

            Join, 3, 17

 

     As Required:

 

      19    s1 e n

            Detach, 12, 18

 

         

          Prove: ALL(a):[aen => f(a)en]

           

          Suppose...

 

            20    x e n

                  Premise

 

          Apply definition of n

 

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

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

                  U Spec, 8

 

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

              => [s1 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]

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

                  Iff-And, 21

 

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

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

                  Split, 22

 

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

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

                  Split, 22

 

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

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

                  Detach, 23, 20

 

            26    x e s

                  Split, 25

 

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

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

                  Split, 25

 

          Apply definiton of n

 

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

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

                  U Spec, 8

 

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

              => [s1 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]

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

                  Iff-And, 28

 

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

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

                  Split, 29

 

          Sufficient: For f(x) e n

 

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

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

                  Split, 29

 

          Apply definition of f

 

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

                  U Spec, 4

 

          As Required:

 

            33    f(x) e s

                  Detach, 32, 26

 

             

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

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

             

              Suppose...

 

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

                        Premise

 

                  

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

                  

                   Suppose...

 

                        35    s1 e q & ALL(c):[c e q => f(c) e q]

                              Premise

 

                        36    s1 e q

                              Split, 35

 

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

                              Split, 35

 

                   Sufficient: f(x) e q

 

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

                              U Spec, 37

 

                   Apply previous result

 

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

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

                              U Spec, 27

 

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

                              Detach, 39, 34

 

                        41    x e q

                              Detach, 40, 35

 

                        42    f(x) e q

                              Detach, 38, 41

 

              As Required:

 

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

                        4 Conclusion, 35

 

          As Required:

 

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

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

                  4 Conclusion, 34

 

          Joining results...

 

            45    f(x) e s

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

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

                  Join, 33, 44

 

            46    f(x) e n

                  Detach, 31, 45

 

     As Required:

 

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

            4 Conclusion, 20

 

         

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

         

          Suppose...

 

            48    x e n

                  Premise

 

          Apply definition of n

 

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

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

                  U Spec, 8

 

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

              => [s1 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]

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

                  Iff-And, 49

 

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

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

                  Split, 50

 

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

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

                  Split, 50

 

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

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

                  Detach, 51, 48

 

            54    x e s

                  Split, 53

 

     As Required:

 

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

            4 Conclusion, 48

 

         

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

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

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

         

          Suppose...

 

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

                  Premise

 

            57    Set(p)

                  Split, 56

 

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

                  Split, 56

 

             

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

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

             

              Suppose...

 

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

                        Premise

 

                  

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

                  

                   Suppose...

 

                        60    x e n

                              Premise

 

                   Apply definition of n

 

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

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

                              U Spec, 8

 

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

                        => [s1 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]

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

                              Iff-And, 61

 

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

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

                              Split, 62

 

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

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

                              Split, 62

 

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

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

                              Detach, 63, 60

 

                        66    x e s

                              Split, 65

 

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

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

                              Split, 65

 

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

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

                              U Spec, 67

 

                       

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

                       

                        Suppose...

 

                              69    y e p

                                    Premise

 

                              70    y e p => y e n

                                    U Spec, 58

 

                              71    y e n

                                    Detach, 70, 69

 

                              72    y e n => y e s

                                    U Spec, 55

 

                              73    y e s

                                    Detach, 72, 71

 

                   As Required:

 

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

                              4 Conclusion, 69

 

                   Joining results...

 

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

                              Join, 57, 74

 

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

                              Detach, 68, 75

 

                        77    x e p

                              Detach, 76, 59

 

              As Required:

 

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

                        4 Conclusion, 60

 

          As Required:

 

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

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

                  4 Conclusion, 59

 

     Induction principle

    

     As Required:

 

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

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

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

            4 Conclusion, 56

 

     Joining results...

 

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

            Join, 7, 55

 

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

            Join, 81, 19

 

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

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

            Join, 82, 47

 

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

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

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

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

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

            Join, 83, 80

 

As Required:

 

85    ALL(s):ALL(s1):ALL(f):[Set(s)

     & s1 e s

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

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

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

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

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

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

      4 Conclusion, 1