THEOREM

*******

 

Assume the existence of an infinite set m. We can select a subset n of m such that: n = {n0, s(n0), s(s(n0))...}, and each of the Peano Axioms can be shown to hold n on (n,s,n0).

 

PA1  n0 e n          (Lines 20-30)

 

PA2  s: n --> n      (Lines 31-59)

 

PA3  s is injective  (Lines 60-71)

 

PA4  s(x)=/=n0       (Lines 72-77)

 

PA5  Induction       (Lines 78-105)

 

Only direct proof is used. An axiom of set theory is used only once (on line 8, the Subset Axiom, equivalent to Specification in ZFC).

 

 

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

 

 

PROOF

*****

 

Assume the existence of an infinite set m (after Dedekind)

 

1     Set(m)

      Axiom

 

Define: s

 

s: m --> m

 

2     ALL(a):[a e m => s(a) e m]

      Axiom

 

s is injective

 

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

      Axiom

 

s is not surjective

 

4     EXIST(a):[a e m & ALL(b):[b e m => ~s(b)=a]]

      Axiom

 

Define: n0

 

5     n0 e m & ALL(b):[b e m => ~s(b)=n0]

      E Spec, 4

 

6     n0 e m

      Split, 5

 

7     ALL(b):[b e m => ~s(b)=n0]

      Split, 5

 

 

Construct n

 

Apply the Subset Axiom

 

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

    & n0 e b

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

    => a e b]]]

      Subset, 1

 

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

    & n0 e b

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

    => a e b]]

      E Spec, 8

 

 

Define: n  

 

Informally, n = {n0, s(n0), s(s(n0))...}

 

10   Set(n)

      Split, 9

 

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

    & n0 e b

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

    => a e b]]

      Split, 9

 

   

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

   

    Suppose...

 

      12   x e n

            Premise

 

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

         & n0 e b

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

         => x e b]

            U Spec, 11

 

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

         & n0 e b

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

         => x e b]]

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

         & n0 e b

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

         => x e b] => x e n]

            Iff-And, 13

 

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

         & n0 e b

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

         => x e b]

            Split, 14

 

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

         & n0 e b

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

         => x e b] => x e n

            Split, 14

 

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

         & n0 e b

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

         => x e b]

            Detach, 15, 12

 

      18   x e m

            Split, 17

 

As Required:

 

19   ALL(a):[a e n => a e m]

      4 Conclusion, 12

 

 

PA1

 

Prove: n0 e n

 

20   n0 e n <=> n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

    & n0 e b

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

    => n0 e b]

      U Spec, 11

 

21   [n0 e n => n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

    & n0 e b

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

    => n0 e b]]

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

    & n0 e b

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

    => n0 e b] => n0 e n]

      Iff-And, 20

 

22   n0 e n => n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

    & n0 e b

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

    => n0 e b]

      Split, 21

 

Sufficient: For n0 e n

 

23   n0 e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

    & n0 e b

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

    => n0 e b] => n0 e n

      Split, 21

 

   

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

   

    Suppose...

 

      24   Set(y) & ALL(c):[c e y => c e m]

         & n0 e y

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

            Premise

 

      25   Set(y)

            Split, 24

 

      26   ALL(c):[c e y => c e m]

            Split, 24

 

      27   n0 e y

            Split, 24

 

As Required:

 

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

    & n0 e b

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

    => n0 e b]

      4 Conclusion, 24

 

29   n0 e m

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

    & n0 e b

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

    => n0 e b]

      Join, 6, 28

 

 

PA1

 

30   n0 e n

      Detach, 23, 29

 

   

    PA2

   

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

   

    Suppose...

 

      31   x e n

            Premise

 

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

         & n0 e b

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

         => s(x) e b]

            U Spec, 11

 

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

         & n0 e b

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

         => s(x) e b]]

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

         & n0 e b

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

         => s(x) e b] => s(x) e n]

            Iff-And, 32

 

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

         & n0 e b

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

         => s(x) e b]

            Split, 33

 

    Sufficient: For s(x) e n

 

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

         & n0 e b

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

         => s(x) e b] => s(x) e n

            Split, 33

 

      36   x e m => s(x) e m

            U Spec, 2

 

      37   x e n => x e m

            U Spec, 19

 

      38   x e m

            Detach, 37, 31

 

    As Required:

 

      39   s(x) e m

            Detach, 36, 38

 

        

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

                & n0 e b

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

                => s(x) e b]

        

         Suppose...

 

            40   Set(y) & ALL(c):[c e y => c e m]

             & n0 e y

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

                  Premise

 

            41   Set(y)

                  Split, 40

 

            42   ALL(c):[c e y => c e m]

                  Split, 40

 

            43   n0 e y

                  Split, 40

 

            44   ALL(c):[c e y => s(c) e y]

                  Split, 40

 

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

             & n0 e b

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

             => x e b]

                  U Spec, 11

 

            46   [x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

             & n0 e b

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

             => x e b]]

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

             & n0 e b

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

             => x e b] => x e n]

                  Iff-And, 45

 

            47   x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

             & n0 e b

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

             => x e b]

                  Split, 46

 

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

             & n0 e b

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

             => x e b] => x e n

                  Split, 46

 

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

             & n0 e b

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

             => x e b]

                  Detach, 47, 31

 

            50   x e m

                  Split, 49

 

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

             & n0 e b

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

             => x e b]

                  Split, 49

 

            52   Set(y) & ALL(c):[c e y => c e m]

             & n0 e y

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

             => x e y

                  U Spec, 51

 

            53   x e y

                  Detach, 52, 40

 

            54   x e y => s(x) e y

                  U Spec, 44

 

            55   s(x) e y

                  Detach, 54, 53

 

    As Required:

 

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

         & n0 e b

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

         => s(x) e b]

            4 Conclusion, 40

 

      57   s(x) e m

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

         & n0 e b

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

         => s(x) e b]

            Join, 39, 56

 

      58   s(x) e n

            Detach, 35, 57

 

PA2

 

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

      4 Conclusion, 31

 

   

    PA3

   

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

   

    Suppose...

 

      60   x e n & y e n

            Premise

 

      61   x e n

            Split, 60

 

      62   y e n

            Split, 60

 

      63   ALL(b):[x e m & b e m => [s(x)=s(b) => x=b]]

            U Spec, 3

 

      64   x e m & y e m => [s(x)=s(y) => x=y]

            U Spec, 63

 

      65   x e n => x e m

            U Spec, 19

 

      66   x e m

            Detach, 65, 61

 

      67   y e n => y e m

            U Spec, 19

 

      68   y e m

            Detach, 67, 62

 

      69   x e m & y e m

            Join, 66, 68

 

      70   s(x)=s(y) => x=y

            Detach, 64, 69

 

PA3

 

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

      4 Conclusion, 60

 

   

    PA4

   

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

   

    Suppose...

 

      72   x e n

            Premise

 

      73   x e m => ~s(x)=n0

            U Spec, 7

 

      74   x e n => x e m

            U Spec, 19

 

      75   x e m

            Detach, 74, 72

 

      76   ~s(x)=n0

            Detach, 73, 75

 

PA4

 

77   ALL(a):[a e n => ~s(a)=n0]

      4 Conclusion, 72

 

   

    PA5 (Induction)

   

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

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

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

   

    Suppose...

 

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

            Premise

 

      79   Set(p)

            Split, 78

 

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

            Split, 78

 

        

         Prove: n0 e p & ALL(b):[b e p => s(b) e p]

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

        

         Suppose...

 

            81   n0 e p & ALL(b):[b e p => s(b) e p]

                  Premise

 

            82   n0 e p

                  Split, 81

 

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

                  Split, 81

 

            

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

            

             Suppose...

 

                  84   x e n

                        Premise

 

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

                 & n0 e b

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

                 => x e b]

                        U Spec, 11

 

                  86   [x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

                 & n0 e b

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

                  => x e b]]

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

                 & n0 e b

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

                 => x e b] => x e n]

                        Iff-And, 85

 

                  87   x e n => x e m & ALL(b):[Set(b) & ALL(c):[c e b => c e m]

                 & n0 e b

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

                 => x e b]

                        Split, 86

 

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

                 & n0 e b

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

                 => x e b] => x e n

                        Split, 86

 

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

                 & n0 e b

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

                 => x e b]

                        Detach, 87, 84

 

                  90   x e m

                        Split, 89

 

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

                 & n0 e b

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

                 => x e b]

                        Split, 89

 

             Sufficient: For x e p

 

                  92   Set(p) & ALL(c):[c e p => c e m]

                 & n0 e p

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

                 => x e p

                        U Spec, 91

 

                        93   y e p

                              Premise

 

                        94   y e p => y e n

                              U Spec, 80

 

                        95   y e n

                              Detach, 94, 93

 

                        96   y e n => y e m

                              U Spec, 19

 

                        97   y e m

                              Detach, 96, 95

 

             As Required:

 

                  98   ALL(c):[c e p => c e m]

                        4 Conclusion, 93

 

                  99   Set(p) & ALL(c):[c e p => c e m]

                        Join, 79, 98

 

                  100  Set(p) & ALL(c):[c e p => c e m] & n0 e p

                        Join, 99, 82

 

                  101  Set(p) & ALL(c):[c e p => c e m] & n0 e p

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

                        Join, 100, 83

 

                  102  x e p

                        Detach, 92, 101

 

         As Required:

 

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

                  4 Conclusion, 84

 

    As Required:

 

      104  n0 e p & ALL(b):[b e p => s(b) e p]

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

            4 Conclusion, 81

 

PA5  (Induction axiom)

 

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

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

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

      4 Conclusion, 78