Definition of the set of natural numbers proposed by WM:

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

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

(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     1+1=1

      Axiom

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

      Axiom

     '=>'

     Prove: ALL(a):[a e n

            => ALL(b):[1 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=1

            U Spec, 2

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

            Iff-And, 4

      6     x e n => x=1

            Split, 5

      7     x=1 => x e n

            Split, 5

      8     x=1

            Detach, 6, 3

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

          Suppose...

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

                  Premise

            10    1 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):[1 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):[1 e b & ALL(c):[c e b => c+1 e b] => a e b]]

      4 Conclusion, 3

     '<='

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

            => a e n]

     Suppose...

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

            Premise

     Apply definition of n

      16    x e n <=> x=1

            U Spec, 2

      17    [x e n => x=1] & [x=1 => x e n]

            Iff-And, 16

      18    x e n => x=1

            Split, 17

      19    x=1 => x e n

            Split, 17

     Apply premise

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

            U Spec, 15

      21    1 e n <=> 1=1

            U Spec, 2

      22    [1 e n => 1=1] & [1=1 => 1 e n]

            Iff-And, 21

      23    1 e n => 1=1

            Split, 22

      24    1=1 => 1 e n

            Split, 22

      25    1=1

            Reflex

      26    1 e n

            Detach, 24, 25

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

          Suppose...

            27    y e n

                  Premise

          Apply definition of n

            28    y e n <=> y=1

                  U Spec, 2

            29    [y e n => y=1] & [y=1 => y e n]

                  Iff-And, 28

            30    y e n => y=1

                  Split, 29

            31    y=1 => y e n

                  Split, 29

            32    y=1

                  Detach, 30, 27

            33    y=1+1

                  Substitute, 1, 32

            34    y=y+1

                  Substitute, 32, 33

            35    y+1 e n

                  Substitute, 34, 27

     As Required:

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

            4 Conclusion, 27

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

            Join, 26, 36

      38    x e n

            Detach, 20, 37

As Required:

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

     => a e n]

      4 Conclusion, 15

Combining results...

40    ALL(a):[[a e n

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

     => a e n]]

      Join, 14, 39

As Required:

41    ALL(a):[a e n

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

      Iff-And, 40