Here we apply WM's proposed definition of the natural numbers to obtain:

 

1 e n

1+1 e n

1+1+1 e n

 

ALL(a):[aen => EXIST(b):[ben & b=a+1]]

 

2=1+1

3=2+1

4=3+1

 

 

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

 

 

Define: n  (proposed by WM)

*********

 

1     ALL(a):[a e n

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

      Axiom

 

Prove: 1en

 

Apply definition of 1

 

2     1 e n

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

      U Spec, 1

 

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

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

      Iff-And, 2

 

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

      Split, 3

 

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

      Split, 3

 

    

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

    

     Suppose...

 

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

            Premise

 

      7     1 e p

            Split, 6

 

As Required:

 

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

      4 Conclusion, 6

 

As Required:

 

9     1 e n

      Detach, 5, 8

 

Prove: 1+1 e n

 

Apply definiton of n

 

10    1+1 e n

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

      U Spec, 1

 

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

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

      Iff-And, 10

 

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

      Split, 11

 

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

      Split, 11

 

    

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

    

     Suppose...

 

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

            Premise

 

      15    1 e p

            Split, 14

 

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

            Split, 14

 

      17    1 e p => 1+1 e p

            U Spec, 16

 

      18    1+1 e p

            Detach, 17, 15

 

As Required:

 

19    ALL(bp):[1 e bp & ALL(c):[c e bp => c+1 e bp] => 1+1 e bp]

      4 Conclusion, 14

 

As Required:

 

20    1+1 e n

      Detach, 13, 19

 

Prove: 1+1+1 e n

 

Apply definition of n

 

21    1+1+1 e n

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

      U Spec, 1

 

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

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

      Iff-And, 21

 

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

      Split, 22

 

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

      Split, 22

 

    

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

    

     Suppose...

 

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

            Premise

 

      26    1 e p

            Split, 25

 

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

            Split, 25

 

      28    1+1 e p => 1+1+1 e p

            U Spec, 27

 

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

            Detach, 12, 20

 

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

            U Spec, 29

 

      31    1+1 e p

            Detach, 30, 25

 

      32    1+1+1 e p

            Detach, 28, 31

 

As Required:

 

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

      4 Conclusion, 25

 

As Required:

 

34    1+1+1 e n

      Detach, 24, 33

 

    

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

    

     Suppose...

 

      35    x e n

            Premise

 

     Apply definition n

 

      36    x e n

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

            U Spec, 1

 

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

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

            Iff-And, 36

 

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

            Split, 37

 

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

            Split, 37

 

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

            Detach, 38, 35

 

     Apply definition of n

 

      41    x+1 e n

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

            U Spec, 1

 

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

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

            Iff-And, 41

 

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

            Split, 42

 

     Sufficient:

 

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

            Split, 42

 

         

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

         

          Suppose...

 

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

                  Premise

 

            46    1 e p

                  Split, 45

 

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

                  Split, 45

 

          Sufficient: x+1 e p

 

            48    x e p => x+1 e p

                  U Spec, 47

 

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

                  U Spec, 40

 

            50    x e p

                  Detach, 49, 45

 

            51    x+1 e p

                  Detach, 48, 50

 

     As Required:

 

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

            4 Conclusion, 45

 

      53    x+1 e n

            Detach, 44, 52

 

      54    x+1=x+1

            Reflex

 

      55    x+1 e n & x+1=x+1

            Join, 53, 54

 

     Generalizing...

 

      56    EXIST(b):[b e n & b=x+1]

            E Gen, 55

 

As Required:

 

57    ALL(a):[a e n => EXIST(b):[b e n & b=a+1]]

      4 Conclusion, 35

 

Prove: 2=1+1

 

Apply previous result

 

58    1 e n => EXIST(b):[b e n & b=1+1]

      U Spec, 57

 

59    EXIST(b):[b e n & b=1+1]

      Detach, 58, 9

 

60    2 e n & 2=1+1

      E Spec, 59

 

61    2 e n

      Split, 60

 

As Required:

 

62    2=1+1

      Split, 60

 

Prove: 3=2+1

 

Apply previous result

 

63    2 e n => EXIST(b):[b e n & b=2+1]

      U Spec, 57

 

64    EXIST(b):[b e n & b=2+1]

      Detach, 63, 61

 

65    3 e n & 3=2+1

      E Spec, 64

 

66    3 e n

      Split, 65

 

As Required:

 

67    3=2+1

      Split, 65

 

Prove: 4=3+1

 

Apply previous result

 

68    3 e n => EXIST(b):[b e n & b=3+1]

      U Spec, 57

 

69    EXIST(b):[b e n & b=3+1]

      Detach, 68, 66

 

70    4 e n & 4=3+1

      E Spec, 69

 

71    4 e n

      Split, 70

 

As Required:

 

72    4=3+1

      Split, 70