THEOREM

*******

Here, we construct an ordering lt (<) on the set of natural numbers n using Peano's Axioms, the Cartesian product and Subset axioms, and the previously constructed add function (+) on n.

Prove: EXIST(lt):ALL(a):ALL(b):[a e n & b e n => [(a,b) e lt <=> EXIST(c):[c e n & a+c=b]]]

In subsequent proofs, we will use the more standard infix '<' notation.

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

PEANO'S AXIOMS

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

1     Set(n)

      Axiom

2     1 e n

      Axiom

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

      Axiom

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

      Axiom

5     ALL(a):[a e n => ~s(a)=1]

      Axiom

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

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

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

      Axiom

FROM PREVIOUS RESULTS

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

Define: + on n

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

      Axiom

8     ALL(a):[a e n => a+1=s(a)]

      Axiom

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

      Axiom

PROOF

*****

Apply Cartesian Product axiom

10    ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b
     <=> c1 e a1 & c2 e a2]]]

      Cart Prod

11    ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b
     <=> c1 e n & c2 e a2]]]

      U Spec, 10

12    Set(n) & Set(n) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

      U Spec, 11

13    Set(n) & Set(n)

      Join, 1, 1

14    EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n]]

      Detach, 12, 13

15    Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      E Spec, 14

Define: n2

**********

The set of ordered pairs of natural numbers

16    Set'(n2)

      Split, 15

17    ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      Split, 15

Apply Subset axiom

18    EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & EXIST(c):[c e n & a+c=b]]]

      Subset, 16

19    Set'(lt) & ALL(a):ALL(b):[(a,b) e lt <=> (a,b) e n2 & EXIST(c):[c e n & a+c=b]]

      E Spec, 18

Define: lt

**********

(x,y) e lt means x is less than y

20    Set'(lt)

      Split, 19

21    ALL(a):ALL(b):[(a,b) e lt <=> (a,b) e n2 & EXIST(c):[c e n & a+c=b]]

      Split, 19

     Recast definition without reference to n2

     Prove: ALL(a):ALL(b):[a e n & b e n

            => [(a,b) e lt <=> EXIST(c):[c e n & a+c=b]]]

     Suppose...

      22    x e n & y e n

            Premise

      23    x e n

            Split, 22

      24    y e n

            Split, 22

          '=>'

          Prove: (x,y) e lt => EXIST(c):[c e n & x+c=y]

          Suppose...

            25    (x,y) e lt

                  Premise

          Apply definition of lt

            26    ALL(b):[(x,b) e lt <=> (x,b) e n2 & EXIST(c):[c e n & x+c=b]]

                  U Spec, 21

            27    (x,y) e lt <=> (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  U Spec, 26

            28    [(x,y) e lt => (x,y) e n2 & EXIST(c):[c e n & x+c=y]]

              & [(x,y) e n2 & EXIST(c):[c e n & x+c=y] => (x,y) e lt]

                  Iff-And, 27

            29    (x,y) e lt => (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  Split, 28

            30    (x,y) e n2 & EXIST(c):[c e n & x+c=y] => (x,y) e lt

                  Split, 28

            31    (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  Detach, 29, 25

            32    (x,y) e n2

                  Split, 31

            33    EXIST(c):[c e n & x+c=y]

                  Split, 31

     As Required:

      34    (x,y) e lt => EXIST(c):[c e n & x+c=y]

            4 Conclusion, 25

          '<='

          Prove: EXIST(c):[c e n & x+c=y] => (x,y) e lt

          Suppose...

            35    EXIST(c):[c e n & x+c=y]

                  Premise

          Apply definition of lt

            36    ALL(b):[(x,b) e lt <=> (x,b) e n2 & EXIST(c):[c e n & x+c=b]]

                  U Spec, 21

            37    (x,y) e lt <=> (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  U Spec, 36

            38    [(x,y) e lt => (x,y) e n2 & EXIST(c):[c e n & x+c=y]]

              & [(x,y) e n2 & EXIST(c):[c e n & x+c=y] => (x,y) e lt]

                  Iff-And, 37

            39    (x,y) e lt => (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  Split, 38

            40    (x,y) e n2 & EXIST(c):[c e n & x+c=y] => (x,y) e lt

                  Split, 38

            41    ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 17

          Apply definition of n2

            42    (x,y) e n2 <=> x e n & y e n

                  U Spec, 41

            43    [(x,y) e n2 => x e n & y e n]

              & [x e n & y e n => (x,y) e n2]

                  Iff-And, 42

            44    (x,y) e n2 => x e n & y e n

                  Split, 43

            45    x e n & y e n => (x,y) e n2

                  Split, 43

            46    (x,y) e n2

                  Detach, 45, 22

            47    (x,y) e n2 & EXIST(c):[c e n & x+c=y]

                  Join, 46, 35

            48    (x,y) e lt

                  Detach, 40, 47

     As Required:

      49    EXIST(c):[c e n & x+c=y] => (x,y) e lt

            4 Conclusion, 35

     Joining results...

      50    [(x,y) e lt => EXIST(c):[c e n & x+c=y]]

          & [EXIST(c):[c e n & x+c=y] => (x,y) e lt]

            Join, 34, 49

     Apply Iff-And rule

      51    (x,y) e lt <=> EXIST(c):[c e n & x+c=y]

            Iff-And, 50

As Required:

52    ALL(a):ALL(b):[a e n & b e n

     => [(a,b) e lt <=> EXIST(c):[c e n & a+c=b]]]

      4 Conclusion, 22

As Required:

53    EXIST(lt):ALL(a):ALL(b):[a e n & b e n

     => [(a,b) e lt <=> EXIST(c):[c e n & a+c=b]]]

      E Gen, 52