THEOREM

*******

 

Given:

 

  1. Peano systems (n,next,0) and (n',next',0')

 

  2. f: n --> n'   (as defined below)

 

  3. f': n' --> n  (as defined below

 

Prove:

 

  1. f' is the inverse of f, i.e. f is a bijection  (lines 19 - 80)

 

       ALL(a):[a e n => f'(f(a))=a]

 

  2. f is injective  (lines 81 - 92)

 

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

 

  3. f preserves the successor relation  (lines 93 - 117)

 

       ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

 

(This proof was written with the aid of the author's DC Proof 2.0 software available at

http://www.dcproof.com)

 

 

DEFINITIONS

**********

 

Peano system (n,0,next)

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

next is a function on n

 

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

      Axiom

 

next is an injective (1-to-1) function

 

If x has a predecessor, that predecessor is unique.

 

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

      Axiom

 

0 has no predecessor under next

 

5     ALL(a):[a e n => ~next(a)=0]

      Axiom

 

Principle of mathematical induction (PMI) for (n,0,next)

 

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

     => [0 e a & ALL(b):[b e a => next(b) e a]

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

      Axiom

 

 

Peano system (n',0',next')

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

 

7     Set(n')

      Axiom

 

8     0' e n'

      Axiom

 

next' is a function on n'

 

9     ALL(a):[a e n' => next'(a) e n']

      Axiom

 

next' is an injective (1-to-1) function

 

10    ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]

      Axiom

 

0' has no predecessor under next'

 

11    ALL(a):[a e n' => ~next'(a)=0']

      Axiom

 

Principle of mathematical induction (PMI) for (n',0',next')

 

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

     => [0' e a & ALL(b):[b e a => next'(b) e a]

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

      Axiom

 

 

Define: f  (previously constructed)   EquivalentPeanoSystemsA.htm

*********

 

13    ALL(a):[a e n => f(a) e n']

      Axiom

 

14    f(0)=0'

      Axiom

 

15    ALL(a):[a e n => f(next(a))=next'(f(a))]

      Axiom

 

 

Define: f'  (similarly to f)

**********

 

16    ALL(a):[a e n' => f'(a) e n]

      Axiom

 

17    f'(0')=0

      Axiom

 

18    ALL(a):[a e n' => f'(next'(a))=next(f'(a))]

      Axiom

 

 

PROOF

*****

 

Prove: f' is the inverse of f by induction

 

Construct subset p to apply PMI

 

Applying Subset Axiom...

 

19    EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & f'(f(a))=a]]

      Subset, 1

 

20    Set(p) & ALL(a):[a e p <=> a e n & f'(f(a))=a]

      E Spec, 19

 

Define: p

 

21    Set(p)

      Split, 20

 

22    ALL(a):[a e p <=> a e n & f'(f(a))=a]

      Split, 20

 

Apply PMI on n

 

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

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

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

      U Spec, 6

 

    

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

    

     Suppose...

 

      24    x e p

            Premise

 

      25    x e p <=> x e n & f'(f(x))=x

            U Spec, 22

 

      26    [x e p => x e n & f'(f(x))=x]

          & [x e n & f'(f(x))=x => x e p]

            Iff-And, 25

 

      27    x e p => x e n & f'(f(x))=x

            Split, 26

 

      28    x e n & f'(f(x))=x => x e p

            Split, 26

 

      29    x e n & f'(f(x))=x

            Detach, 27, 24

 

      30    x e n

            Split, 29

 

As Required:

 

31    ALL(a):[a e p => a e n]

      4 Conclusion, 24

 

32    Set(p) & ALL(a):[a e p => a e n]

      Join, 21, 31

 

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

 

33    0 e p & ALL(b):[b e p => next(b) e p]

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

      Detach, 23, 32

 

 

Prove: 0 e p  (base case)

 

Apply definition of p

 

34    0 e p <=> 0 e n & f'(f(0))=0

      U Spec, 22

 

35    [0 e p => 0 e n & f'(f(0))=0]

     & [0 e n & f'(f(0))=0 => 0 e p]

      Iff-And, 34

 

36    0 e p => 0 e n & f'(f(0))=0

      Split, 35

 

Sufficient: For 0 e p

 

37    0 e n & f'(f(0))=0 => 0 e p

      Split, 35

 

38    f'(f(0))=0

      Substitute, 14, 17

 

39    0 e n & f'(f(0))=0

      Join, 2, 38

 

As Required:

 

40    0 e p

      Detach, 37, 39

 

    

     Prove: ALL(a):[a e p => next(a) e p]  (inductive case)

    

     Suppose...

 

      41    x e p

            Premise

 

     Apply definition of p for x

 

      42    x e p <=> x e n & f'(f(x))=x

            U Spec, 22

 

      43    [x e p => x e n & f'(f(x))=x]

          & [x e n & f'(f(x))=x => x e p]

            Iff-And, 42

 

      44    x e p => x e n & f'(f(x))=x

            Split, 43

 

      45    x e n & f'(f(x))=x => x e p

            Split, 43

 

      46    x e n & f'(f(x))=x

            Detach, 44, 41

 

      47    x e n

            Split, 46

 

      48    f'(f(x))=x

            Split, 46

 

     Apply definition of p for next(x)

 

      49    next(x) e p <=> next(x) e n & f'(f(next(x)))=next(x)

            U Spec, 22

 

      50    [next(x) e p => next(x) e n & f'(f(next(x)))=next(x)]

          & [next(x) e n & f'(f(next(x)))=next(x) => next(x) e p]

            Iff-And, 49

 

      51    next(x) e p => next(x) e n & f'(f(next(x)))=next(x)

            Split, 50

 

     Sufficient: For next(x) e p

 

      52    next(x) e n & f'(f(next(x)))=next(x) => next(x) e p

            Split, 50

 

     Prove: next(x) e n

 

      53    x e n => next(x) e n

            U Spec, 3

 

     As Required:

 

      54    next(x) e n

            Detach, 53, 47

 

     Prove: f'(f(next(x)))=next(x)

 

      55    f'(f(next(x)))=f'(f(next(x)))

            Reflex

 

      56    x e n => f(next(x))=next'(f(x))

            U Spec, 15

 

      57    f(next(x))=next'(f(x))

            Detach, 56, 47

 

      58    f'(f(next(x)))=f'(next'(f(x)))

            Substitute, 57, 55

 

      59    f(x) e n' => f'(next'(f(x)))=next(f'(f(x)))

            U Spec, 18

 

      60    x e n => f(x) e n'

            U Spec, 13

 

      61    f(x) e n'

            Detach, 60, 47

 

      62    f'(next'(f(x)))=next(f'(f(x)))

            Detach, 59, 61

 

      63    f'(f(next(x)))=next(f'(f(x)))

            Substitute, 62, 58

 

     As Required:

 

      64    f'(f(next(x)))=next(x)

            Substitute, 48, 63

 

      65    next(x) e n & f'(f(next(x)))=next(x)

            Join, 54, 64

 

      66    next(x) e p

            Detach, 52, 65

 

As Required:

 

67    ALL(a):[a e p => next(a) e p]

      4 Conclusion, 41

 

68    0 e p & ALL(a):[a e p => next(a) e p]

      Join, 40, 67

 

As Required:

 

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

      Detach, 33, 68

 

    

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

    

     Suppose...

 

      70    x e n

            Premise

 

      71    x e n => x e p

            U Spec, 69

 

      72    x e p

            Detach, 71, 70

 

      73    x e p <=> x e n & f'(f(x))=x

            U Spec, 22

 

      74    [x e p => x e n & f'(f(x))=x]

          & [x e n & f'(f(x))=x => x e p]

            Iff-And, 73

 

      75    x e p => x e n & f'(f(x))=x

            Split, 74

 

      76    x e n & f'(f(x))=x => x e p

            Split, 74

 

      77    x e n & f'(f(x))=x

            Detach, 75, 72

 

      78    x e n

            Split, 77

 

      79    f'(f(x))=x

            Split, 77

 

 

f' is the inverse of f  (f is a bijection)

 

As Required:

 

80    ALL(a):[a e n => f'(f(a))=a]

      4 Conclusion, 70

 

    

     Prove: f is injective

    

     Suppose...

 

      81    x e n & y e n

            Premise

 

      82    x e n

            Split, 81

 

      83    y e n

            Split, 81

 

         

          Prove: f(x)=f(y) => x=y

         

          Suppose...

 

            84    f(x)=f(y)

                  Premise

 

            85    x e n => f'(f(x))=x

                  U Spec, 80

 

            86    f'(f(x))=x

                  Detach, 85, 82

 

            87    f'(f(y))=x

                  Substitute, 84, 86

 

            88    y e n => f'(f(y))=y

                  U Spec, 80

 

            89    f'(f(y))=y

                  Detach, 88, 83

 

            90    x=y

                  Substitute, 87, 89

 

     As Required:

 

      91    f(x)=f(y) => x=y

            4 Conclusion, 84

 

f is injective

 

As Required:

 

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

      4 Conclusion, 81

 

    

     Prove: f preserves successor relation

    

     Suppose...

 

      93    x e n & y e n

            Premise

 

      94    x e n

            Split, 93

 

      95    y e n

            Split, 93

 

          '=>'

         

          Prove: next(x)=y => next'(f(x))=f(y)

         

          Suppose...

 

            96    next(x)=y

                  Premise

 

            97    next'(f(x))=next'(f(x))

                  Reflex

 

            98    x e n => f(next(x))=next'(f(x))

                  U Spec, 15

 

            99    f(next(x))=next'(f(x))

                  Detach, 98, 94

 

            100  next'(f(x))=f(next(x))

                  Substitute, 99, 97

 

            101  next'(f(x))=f(y)

                  Substitute, 96, 100

 

     As Required:

 

      102  next(x)=y => next'(f(x))=f(y)

            4 Conclusion, 96

 

          '<='

         

          Prove: next'(f(x))=f(y) => next(x)=y

         

          Suppose...

 

            103  next'(f(x))=f(y)

                  Premise

 

            104  x e n => f(next(x))=next'(f(x))

                  U Spec, 15

 

            105  f(next(x))=next'(f(x))

                  Detach, 104, 94

 

            106  f(next(x))=f(y)

                  Substitute, 105, 103

 

          Apply injectivity of f

 

            107  ALL(b):[next(x) e n & b e n => [f(next(x))=f(b) => next(x)=b]]

                  U Spec, 92

 

            108  next(x) e n & y e n => [f(next(x))=f(y) => next(x)=y]

                  U Spec, 107

 

            109  x e n => next(x) e n

                  U Spec, 3

 

            110  next(x) e n

                  Detach, 109, 94

 

            111  next(x) e n & y e n

                  Join, 110, 95

 

            112  f(next(x))=f(y) => next(x)=y

                  Detach, 108, 111

 

            113  next(x)=y

                  Detach, 112, 106

 

     As Required:

 

      114  next'(f(x))=f(y) => next(x)=y

            4 Conclusion, 103

 

      115  [next(x)=y => next'(f(x))=f(y)]

          & [next'(f(x))=f(y) => next(x)=y]

            Join, 102, 114

 

      116  next(x)=y <=> next'(f(x))=f(y)

            Iff-And, 115

 

f preserves successor relation

 

As Required:

 

117  ALL(a):ALL(b):[a e n & b e n => [next(a)=b <=> next'(f(a))=f(b)]]

      4 Conclusion, 93