THEOREM

*******

 

Strong induction follows from weak (ordinary) induction

 

Source: http://www.oxfordmathcenter.com/drupal7/node/485

 

 

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

 

 

 

AXIOMS/DEFINITIONS

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

Define: +

 

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

      Axiom

 

Define: <=

 

5     ALL(a):ALL(b):[a e n & b e n => [a<=b <=> EXIST(c):[c e n & a+c=b]]]

      Axiom

 

Required Properties of <=

 

6     ALL(a):[a e n => [a<=0 => a=0]]

      Axiom

 

7     ALL(a):[Set(a) => ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e a]] & b+1 e a

    => ALL(c):[c e n => [c<=b+1 => c e a]]]]]

      Axiom

 

 

WEAK (ORDINARY) INDUCTION HOLDS (USING +1)

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

 

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

    => [0 e a & ALL(b):[b e a => b+1 e a]

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

      Axiom

 

   

    Let p be a subset of n

 

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

            Premise

 

      10   Set(p)

            Split, 9

 

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

            Split, 9

 

        

         Prove: 0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

                => ALL(b):[b e p => b+1 e p]

        

         Suppose...

 

            12   0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

                  Premise

 

            13   0 e p

                  Split, 12

 

            14   ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

                  Split, 12

 

        

        Prove: ALL(a):[a e n => ALL(b):[b e n => [b<=a => b e p]]]  (by ordinary induction)

        

         Construct the set of natural numbers for which this is true.

        

         Apply Subset Axiom

 

            15   EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]]

                  Subset, 1

 

            16   Set(q) & ALL(a):[a e q <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]

                  E Spec, 15

 

        

         Define: q

 

            17   Set(q)

                  Split, 16

 

            18   ALL(a):[a e q <=> a e n & ALL(b):[b e n => [b<=a => b e p]]]

                  Split, 16

 

        

         Apply Ordinary Induction for subset q

 

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

             => [0 e q & ALL(b):[b e q => b+1 e q]

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

                  U Spec, 8

 

            

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

            

             Suppose...

 

                  20   x e q

                        Premise

 

             Apply definition of q

 

                  21   x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

                        U Spec, 18

 

                  22   [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

                 & [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

                        Iff-And, 21

 

                  23   x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Split, 22

 

                  24   x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

                        Split, 22

 

                  25   x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Detach, 23, 20

 

                  26   x e n

                        Split, 25

 

         As Required:

 

            27   ALL(b):[b e q => b e n]

                  4 Conclusion, 20

 

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

                  Join, 17, 27

 

        

         Sufficient: For ALL(b):[b e n => b e q]

 

            29   0 e q & ALL(b):[b e q => b+1 e q]

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

                  Detach, 19, 28

 

        

         BASIS STEP

         **********

        

         Prove: 0 e q

        

         Apply definition of q

 

            30   0 e q <=> 0 e n & ALL(b):[b e n => [b<=0 => b e p]]

                  U Spec, 18

 

            31   [0 e q => 0 e n & ALL(b):[b e n => [b<=0 => b e p]]]

             & [0 e n & ALL(b):[b e n => [b<=0 => b e p]] => 0 e q]

                  Iff-And, 30

 

            32   0 e q => 0 e n & ALL(b):[b e n => [b<=0 => b e p]]

                  Split, 31

 

         Sufficient: For 0 e q

 

            33   0 e n & ALL(b):[b e n => [b<=0 => b e p]] => 0 e q

                  Split, 31

 

            

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

            

             Suppose...

 

                  34   x e n

                        Premise

 

                

                 Prove: x<=0 => x e p

                

                 Suppose...

 

                        35   x<=0

                              Premise

 

                 Apply property of <=

 

                        36   x e n => [x<=0 => x=0]

                              U Spec, 6

 

                        37   x<=0 => x=0

                              Detach, 36, 34

 

                        38   x=0

                              Detach, 37, 35

 

                        39   x e p

                              Substitute, 38, 13

 

             As Required:

 

                  40   x<=0 => x e p

                        4 Conclusion, 35

 

         As Required:

 

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

                  4 Conclusion, 34

 

            42   0 e n & ALL(b):[b e n => [b<=0 => b e p]]

                  Join, 2, 41

 

         As Required:

 

            43   0 e q

                  Detach, 33, 42

 

            

             INDUCTIVE STEP

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

            

             Prove: ALL(b):[b e q => b+1 e q]

            

             Suppose...

 

                  44   x e q

                        Premise

 

             Apply definition of q for x

 

                  45   x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

                        U Spec, 18

 

                  46   [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

                 & [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

                        Iff-And, 45

 

                  47   x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Split, 46

 

                  48   x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

                        Split, 46

 

                  49   x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Detach, 47, 44

 

                  50   x e n

                        Split, 49

 

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

                        Split, 49

 

             Apply definition of q for x+1

 

                  52   x+1 e q <=> x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]

                        U Spec, 18

 

                  53   [x+1 e q => x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]]

                 & [x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]] => x+1 e q]

                        Iff-And, 52

 

                  54   x+1 e q => x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]]

                        Split, 53

 

             Sufficient: For x+1 in q

 

                  55   x+1 e n & ALL(b):[b e n => [b<=x+1 => b e p]] => x+1 e q

                        Split, 53

 

             Apply definition of +

 

                  56   ALL(b):[x e n & b e n => x+b e n]

                        U Spec, 4

 

                  57   x e n & 1 e n => x+1 e n

                        U Spec, 56

 

                  58   x e n & 1 e n

                        Join, 50, 3

 

                  59   x+1 e n

                        Detach, 57, 58

 

             Apply premise

 

                  60   x e n => [ALL(c):[c e n => [c<=x => c e p]] => x+1 e p]

                        U Spec, 14

 

                  61   ALL(c):[c e n => [c<=x => c e p]] => x+1 e p

                        Detach, 60, 50

 

                  62   x+1 e p

                        Detach, 61, 51

 

             Apply property of <=

 

                  63   Set(p) => ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] & b+1 e p

                 => ALL(c):[c e n => [c<=b+1 => c e p]]]]

                        U Spec, 7

 

                  64   ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] & b+1 e p

                 => ALL(c):[c e n => [c<=b+1 => c e p]]]]

                        Detach, 63, 10

 

                  65   x e n => [ALL(c):[c e n => [c<=x => c e p]] & x+1 e p

                 => ALL(c):[c e n => [c<=x+1 => c e p]]]

                        U Spec, 64

 

                  66   ALL(c):[c e n => [c<=x => c e p]] & x+1 e p

                 => ALL(c):[c e n => [c<=x+1 => c e p]]

                        Detach, 65, 50

 

                  67   ALL(b):[b e n => [b<=x => b e p]] & x+1 e p

                        Join, 51, 62

 

                  68   ALL(c):[c e n => [c<=x+1 => c e p]]

                        Detach, 66, 67

 

                  69   x+1 e n & ALL(c):[c e n => [c<=x+1 => c e p]]

                        Join, 59, 68

 

                  70   x+1 e q

                        Detach, 55, 69

 

         As Required:

 

            71   ALL(b):[b e q => b+1 e q]

                  4 Conclusion, 44

 

         Joining results...

 

            72   0 e q & ALL(b):[b e q => b+1 e q]

                  Join, 43, 71

 

            73   ALL(b):[b e n => b e q]

                  Detach, 29, 72

 

            

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

            

             Suppose...

 

                  74   x e n

                        Premise

 

                  75   x e n => x e q

                        U Spec, 73

 

                  76   x e q

                        Detach, 75, 74

 

             Apply definition of q

 

                  77   x e q <=> x e n & ALL(b):[b e n => [b<=x => b e p]]

                        U Spec, 18

 

                  78   [x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]]

                 & [x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q]

                        Iff-And, 77

 

                  79   x e q => x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Split, 78

 

                  80   x e n & ALL(b):[b e n => [b<=x => b e p]] => x e q

                        Split, 78

 

                  81   x e n & ALL(b):[b e n => [b<=x => b e p]]

                        Detach, 79, 76

 

                  82   x e n

                        Split, 81

 

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

                        Split, 81

 

         As Required:

 

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

                  4 Conclusion, 74

 

            

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

            

             Suppose...

 

                  85   x e p

                        Premise

 

                  86   x e p => x e n

                        U Spec, 11

 

                  87   x e n

                        Detach, 86, 85

 

             Apply premise

 

                  88   x e n => [ALL(c):[c e n => [c<=x => c e p]] => x+1 e p]

                        U Spec, 14

 

                  89   ALL(c):[c e n => [c<=x => c e p]] => x+1 e p

                        Detach, 88, 87

 

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

                        U Spec, 84

 

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

                        Detach, 90, 87

 

                  92   x+1 e p

                        Detach, 89, 91

 

         As Required:

 

            93   ALL(b):[b e p => b+1 e p]

                  4 Conclusion, 85

 

         Apply Ordinary Induction for subset p

 

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

             => [0 e p & ALL(b):[b e p => b+1 e p]

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

                  U Spec, 8

 

            95   0 e p & ALL(b):[b e p => b+1 e p]

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

                  Detach, 94, 9

 

            96   0 e p & ALL(b):[b e p => b+1 e p]

                  Join, 13, 93

 

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

                  Detach, 95, 96

 

    As Required:

 

      98   0 e p & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e p]] => b+1 e p]]

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

            4 Conclusion, 12

 

 

STRONG INDUCTION HOLDS

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

 

As Required:

 

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

    => [0 e a & ALL(b):[b e n => [ALL(c):[c e n => [c<=b => c e a]] => b+1 e a]]

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

      4 Conclusion, 9