INTRODUCTION

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

 

Definition of the set of natural numbers proposed by WM (version 2.0):

 

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

                            

 

Unfortunately, this definition is satisfied by the conditions, 0+1=0 and n = {0}.

 

Notice that 1 has not been defined to be a natural number. Addition on has also not been defined at all. So, WM's use of the '+1' notation is a bit misleading. It is really a successor function using a unary, post-fix notation.

 

 

(This proof was written with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )

 

 

AXIOMS

******

 

1     0+1=0

      Axiom

 

Informally, n = {0}

 

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

      Axiom

 

    

     PROOF

     *****

    

     '=>'

    

     Prove: ALL(a):[a e n

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

    

    

     Suppose...

 

      3     x e n

            Premise

 

     Apply definition of n

 

      4     x e n <=> x=0

            U Spec, 2

 

      5     [x e n => x=0] & [x=0 => x e n]

            Iff-And, 4

 

      6     x e n => x=0

            Split, 5

 

      7     x=0 => x e n

            Split, 5

 

      8     x=0

            Detach, 6, 3

 

         

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

         

          Suppose...

 

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

                  Premise

 

            10    0 e p

                  Split, 9

 

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

                  Split, 9

 

            12    x e p

                  Substitute, 8, 10

 

     As Required:

 

      13    ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => x e b]

            4 Conclusion, 9

 

As Required:

 

14    ALL(a):[a e n

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

      4 Conclusion, 3

 

    

     '<='

    

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

            => a e n]

    

     Suppose...

 

      15    ALL(b):[0 e b & ALL(c):[c e b => c+1 e b] => x e b]

            Premise

 

     Sufficient: x e n

 

      16    0 e n & ALL(c):[c e n => c+1 e n] => x e n

            U Spec, 15

 

     Apply definition of n

 

      17    0 e n <=> 0=0

            U Spec, 2

 

      18    [0 e n => 0=0] & [0=0 => 0 e n]

            Iff-And, 17

 

      19    0 e n => 0=0

            Split, 18

 

      20    0=0 => 0 e n

            Split, 18

 

      21    0=0

            Reflex

 

      22    0 e n

            Detach, 20, 21

 

         

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

         

          Suppose...

 

            23    y e n

                  Premise

 

          Apply definition of n

 

            24    y e n <=> y=0

                  U Spec, 2

 

            25    [y e n => y=0] & [y=0 => y e n]

                  Iff-And, 24

 

            26    y e n => y=0

                  Split, 25

 

            27    y=0 => y e n

                  Split, 25

 

            28    y=0

                  Detach, 26, 23

 

            29    y+1=y

                  Substitute, 28, 1

 

            30    y+1 e n

                  Substitute, 29, 23

 

     As Required:

 

      31    ALL(c):[c e n => c+1 e n]

            4 Conclusion, 23

 

     Joining results...

 

      32    0 e n & ALL(c):[c e n => c+1 e n]

            Join, 22, 31

 

      33    x e n

            Detach, 16, 32

 

As Required:

 

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

     => a e n]

      4 Conclusion, 15

 

Joining results...

 

35    ALL(a):[[a e n

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

     => a e n]]

      Join, 14, 34

 

As Required:

 

36    ALL(a):[a e n

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

      Iff-And, 35