THEOREM

*******

 

If there is no non-empty subset of N that excludes 0 and that is not "accessible" from the rest of the natural numbers by means of the successor function, then we can derive the Principle of Mathematical Induction.

 

More formally:

 

     ~EXIST(p):EXIST(p'):[Set(p) & Set(p') & ALL(b):[b e p => b e n]

     & 0 e p

     & ALL(a):[a e p' <=> a e n & ~a e p]

     & ~Accessible(p,p')]

 

     => Induction

 

where 'Accessible' and 'Induction' are as defined below (lines 4-5).

 

 

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

 

 

PROOF

*****

 

1     Set(n)

      Axiom

 

From Peano's Axioms (other axioms not used):

 

2     0 e n

      Axiom

 

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

      Axiom

 

 

Define: Induction

 

'Induction' means that induction holds on (n,s,0)

 

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

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

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

      Axiom

 

Define: Accessible 

 

'Accessible(x,y)' means subset y of n is accessible from subset x of n by means of s

 

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

    => [Accessible(a,b) <=> EXIST(c):EXIST(d):[c e a & d e b & s(c)=d]]]

      Axiom

 

   

    Proof by contrapositive

   

    Prove: ~Induction

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

            & 0 e p

            & ALL(a):[a e p' <=> a e n & ~a e p]

            & ~Accessible(p,p')]

   

    Suppose induction does NOT hold on (n,s,0)

 

      6     ~Induction

            Premise

 

      Apply definition of Induction

 

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

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

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

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

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

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

            Iff-And, 4

 

 

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

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

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

            Split, 7

 

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

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

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

            Split, 7

 

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

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

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

            Contra, 9

 

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

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

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

            Detach, 10, 6

 

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

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

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

            Quant, 11

 

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

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

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

            Rem DNeg, 12

 

      14   EXIST(a):~~[Set(a) & ALL(b):[b e a => b e n] & ~[0 e a & ALL(b):[b e a => s(b) e a]

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

            Imply-And, 13

 

      15   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & ~[0 e a & ALL(b):[b e a => s(b) e a]

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

            Rem DNeg, 14

 

      16   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & ~~[0 e a & ALL(b):[b e a => s(b) e a] & ~ALL(b):[b e n => b e a]]]

            Imply-And, 15

 

      17   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a & ALL(b):[b e a => s(b) e a] & ~ALL(b):[b e n => b e a]]]

            Rem DNeg, 16

 

      18   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a & ALL(b):[b e a => s(b) e a] & ~~EXIST(b):~[b e n => b e a]]]

            Quant, 17

 

      19   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a & ALL(b):[b e a => s(b) e a] & EXIST(b):~[b e n => b e a]]]

            Rem DNeg, 18

 

      20   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a & ALL(b):[b e a => s(b) e a] & EXIST(b):~~[b e n & ~b e a]]]

            Imply-And, 19

 

      21   EXIST(a):[Set(a) & ALL(b):[b e a => b e n] & [0 e a & ALL(b):[b e a => s(b) e a] & EXIST(b):[b e n & ~b e a]]]

            Rem DNeg, 20

 

      22   Set(p) & ALL(b):[b e p => b e n] & [0 e p & ALL(b):[b e p => s(b) e p] & EXIST(b):[b e n & ~b e p]]

            E Spec, 21

 

    Define: p

 

      23   Set(p)

            Split, 22

 

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

            Split, 22

 

      25   0 e p & ALL(b):[b e p => s(b) e p] & EXIST(b):[b e n & ~b e p]

            Split, 22

 

      26   0 e p

            Split, 25

 

      27   ALL(b):[b e p => s(b) e p]

            Split, 25

 

      28   EXIST(b):[b e n & ~b e p]

            Split, 25

 

      29   x0 e n & ~x0 e p

            E Spec, 28

 

      30   x0 e n

            Split, 29

 

      31   ~x0 e p

            Split, 29

 

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

            Subset, 1

 

      33   Set(p') & ALL(a):[a e p' <=> a e n & ~a e p]

            E Spec, 32

 

    Define: p'

 

      34   Set(p')

            Split, 33

 

      35   ALL(a):[a e p' <=> a e n & ~a e p]

            Split, 33

 

      36   x0 e p' <=> x0 e n & ~x0 e p

            U Spec, 35

 

      37   [x0 e p' => x0 e n & ~x0 e p]

         & [x0 e n & ~x0 e p => x0 e p']

            Iff-And, 36

 

      38   x0 e p' => x0 e n & ~x0 e p

            Split, 37

 

      39   x0 e n & ~x0 e p => x0 e p'

            Split, 37

 

      40   x0 e p'

            Detach, 39, 29

 

    Apply defintion of Accessible(p,p')

 

      41   ALL(b):[ALL(c):[c e p => c e n] & EXIST(c):c e p & ALL(c):[c e b => c e n]

         => [Accessible(p,b) <=> EXIST(c):EXIST(d):[c e p & d e b & s(c)=d]]]

            U Spec, 5

 

      42   ALL(c):[c e p => c e n] & EXIST(c):c e p & ALL(c):[c e p' => c e n]

         => [Accessible(p,p') <=> EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]]

            U Spec, 41

 

      43   EXIST(c):c e p

            E Gen, 26

 

        

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

        

         Suppose...

 

            44   x e p'

                  Premise

 

            45   x e p' <=> x e n & ~x e p

                  U Spec, 35

 

            46   [x e p' => x e n & ~x e p] & [x e n & ~x e p => x e p']

                  Iff-And, 45

 

            47   x e p' => x e n & ~x e p

                  Split, 46

 

            48   x e n & ~x e p => x e p'

                  Split, 46

 

            49   x e n & ~x e p

                  Detach, 47, 44

 

            50   x e n

                  Split, 49

 

    As Required:

 

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

            4 Conclusion, 44

 

      52   ALL(b):[b e p => b e n] & EXIST(c):c e p

            Join, 24, 43

 

      53   ALL(b):[b e p => b e n] & EXIST(c):c e p

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

            Join, 52, 51

 

      54   Accessible(p,p') <=> EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]

            Detach, 42, 53

 

      55   [Accessible(p,p') => EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]]

         & [EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => Accessible(p,p')]

            Iff-And, 54

 

      56   Accessible(p,p') => EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d]

            Split, 55

 

      57   EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => Accessible(p,p')

            Split, 55

 

      58   ~EXIST(c):EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')

            Contra, 56

 

      59   ~~ALL(c):~EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')

            Quant, 58

 

      60   ALL(c):~EXIST(d):[c e p & d e p' & s(c)=d] => ~Accessible(p,p')

            Rem DNeg, 59

 

      61   ALL(c):~~ALL(d):~[c e p & d e p' & s(c)=d] => ~Accessible(p,p')

            Quant, 60

 

      62   ALL(c):ALL(d):~[c e p & d e p' & s(c)=d] => ~Accessible(p,p')

            Rem DNeg, 61

 

      63   ALL(c):ALL(d):~~[c e p & d e p' => ~s(c)=d] => ~Accessible(p,p')

            Imply-And, 62

 

   

    Sufficient: For ~Accessible(p,p')

 

      64   ALL(c):ALL(d):[c e p & d e p' => ~s(c)=d] => ~Accessible(p,p')

            Rem DNeg, 63

 

        

         Prove: ALL(c):ALL(d):[c e p & d e p' => ~s(c)=d]

        

         Suppose...

 

            65   y e p & y' e p'

                  Premise

 

            66   y e p

                  Split, 65

 

            67   y' e p'

                  Split, 65

 

            

             Prove: ~s(y)=y'

            

             Suppose to the contrary...

 

                  68   s(y)=y'

                        Premise

 

                  69   y e p => s(y) e p

                        U Spec, 27

 

                  70   s(y) e p

                        Detach, 69, 66

 

                  71   y' e p

                        Substitute, 68, 70

 

                  72   y' e p' <=> y' e n & ~y' e p

                        U Spec, 35

 

                  73   [y' e p' => y' e n & ~y' e p]

                 & [y' e n & ~y' e p => y' e p']

                        Iff-And, 72

 

                  74   y' e p' => y' e n & ~y' e p

                        Split, 73

 

                  75   y' e n & ~y' e p => y' e p'

                        Split, 73

 

                  76   y' e n & ~y' e p

                        Detach, 74, 67

 

                  77   y' e n

                        Split, 76

 

                  78   ~y' e p

                        Split, 76

 

             Obtain the contradiction...

 

                  79   y' e p & ~y' e p

                        Join, 71, 78

 

         As Required:

 

            80   ~s(y)=y'

                  4 Conclusion, 68

 

    As Required:

 

      81   ALL(c):ALL(d):[c e p & d e p' => ~s(c)=d]

            4 Conclusion, 65

 

      82   ~Accessible(p,p')

            Detach, 64, 81

 

      83   Set(p) & Set(p')

            Join, 23, 34

 

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

            Join, 83, 24

 

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

         & 0 e p

            Join, 84, 26

 

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

         & 0 e p

         & ALL(a):[a e p' <=> a e n & ~a e p]

            Join, 85, 35

 

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

         & 0 e p

         & ALL(a):[a e p' <=> a e n & ~a e p]

         & ~Accessible(p,p')

            Join, 86, 82

 

As Required:

 

88   ~Induction

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

    & 0 e p

    & ALL(a):[a e p' <=> a e n & ~a e p]

    & ~Accessible(p,p')]

      4 Conclusion, 6

 

Apply Contrapositive Rule

 

89   ~EXIST(p):EXIST(p'):[Set(p) & Set(p') & ALL(b):[b e p => b e n]

    & 0 e p

    & ALL(a):[a e p' <=> a e n & ~a e p]

    & ~Accessible(p,p')] => ~~Induction

      Contra, 88

 

As Required:

 

90   ~EXIST(p):EXIST(p'):[Set(p) & Set(p') & ALL(b):[b e p => b e n]

    & 0 e p

    & ALL(a):[a e p' <=> a e n & ~a e p]

    & ~Accessible(p,p')] => Induction

      Rem DNeg, 89