THEOREM 3

*********

 

The bijective mapping from n to n' preserves the successor relations on n and n'

 

 

Outline

*******

 

Line 1            Previous result from Theorem 2

 

Lines 2 - 14      Initial assumptions

 

Lines 15 - 164    Prove successor relations are preserved under f

 

Lines 165 - 167   Generalizing

 

 

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

 

 

PREVIOUS RESULT

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

 

From Theorem 2, the mapping from n to n' is bijective

 

1     ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)

     & z1 e n1

     & ALL(a):[a e n1 => next1(a) e n1]

     & ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]

     & ALL(a):[a e n1 => ~next1(a)=z1]

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

     => [z1 e a & ALL(b):[b e a => next1(b) e a]

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

     & Set(n2)

     & z2 e n2

     & ALL(a):[a e n2 => next2(a) e n2]

     & ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

     & ALL(a):[a e n2 => ~next2(a)=z2]

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

     => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

     => ALL(f):[ALL(a):[a e n1 => f(a) e n2]

     & f(z1)=z2

     & ALL(a):[a e n1 => f(next1(a))=next2(f(a))]

     => ALL(a):[a e n2 => EXIST(b):[b e n1 & f(b)=a]]

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

      Axiom

 

    

     PROOF

     *****

    

     Suppose we have Peano systems (n,0,next) and (n',0',next')

 

      2     Set(n)

          & 0 e n

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

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

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

          & 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]]]

          & Set(n')

          & 0' e n'

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

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

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

          & 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]]]

            Premise

 

    

     Peano's Axioms   (n,0,next)

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

 

      3     Set(n)

            Split, 2

 

      4     0 e n

            Split, 2

 

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

            Split, 2

 

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

            Split, 2

 

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

            Split, 2

 

      8     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]]]

            Split, 2

 

    

     Peano's Axioms    (n',0',next')

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

 

      9     Set(n')

            Split, 2

 

      10    0' e n'

            Split, 2

 

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

            Split, 2

 

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

            Split, 2

 

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

            Split, 2

 

      14    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]]]

            Split, 2

 

         

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

                & f(0)=0'

         

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

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

         

          Suppose...

 

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

              & f(0)=0'

                  Premise

 

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

                  Split, 15

 

            17    f(0)=0'

                  Split, 15

 

             

              '=>'

             

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

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

             

              Suppose...

 

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

                        Premise

 

                  

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

                  

                   Suppose...

 

                        19    x e n & y e n

                              Premise

 

                        20    x e n

                              Split, 19

 

                        21    y e n

                              Split, 19

 

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

                       

                        Suppose...

 

                              22    next(x)=y

                                    Premise

 

                              23    next'(f(x))=next'(f(x))

                                    Reflex

 

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

                                    U Spec, 18

 

                              25    f(next(x))=next'(f(x))

                                    Detach, 24, 20

 

                              26    next'(f(x))=f(next(x))

                                    Substitute, 25, 23

 

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

                                    Substitute, 22, 26

 

                   As Required:

 

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

                              4 Conclusion, 22

 

                        '<='

                       

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

                       

                        Suppose...

 

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

                                    Premise

 

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

                                    U Spec, 18

 

                              31    f(next(x))=next'(f(x))

                                    Detach, 30, 20

 

                              32    f(next(x))=f(y)

                                    Substitute, 29, 31

 

                        Apply Theorem 2

 

                              33      ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n)

                             & z1 e n

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

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

                             & ALL(a):[a e n => ~next1(a)=z1]

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

                             => [z1 e a & ALL(b):[b e a => next1(b) e a]

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

                             & Set(n2)

                             & z2 e n2

                             & ALL(a):[a e n2 => next2(a) e n2]

                             & ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

                             & ALL(a):[a e n2 => ~next2(a)=z2]

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

                             => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

                             & f(z1)=z2

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

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

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

                                    U Spec, 1

 

                              34    ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n)

                             & 0 e n

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

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

                             & ALL(a):[a e n => ~next1(a)=0]

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

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

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

                             & Set(n2)

                             & z2 e n2

                             & ALL(a):[a e n2 => next2(a) e n2]

                             & ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

                             & ALL(a):[a e n2 => ~next2(a)=z2]

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

                             => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

                             & f(0)=z2

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

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

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

                                    U Spec, 33

 

                              35    ALL(n2):ALL(z2):ALL(next2):[Set(n)

                             & 0 e n

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

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

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

                             & 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]]]

                             & Set(n2)

                             & z2 e n2

                             & ALL(a):[a e n2 => next2(a) e n2]

                             & ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

                             & ALL(a):[a e n2 => ~next2(a)=z2]

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

                             => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

                             & f(0)=z2

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

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

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

                                    U Spec, 34

 

                              36    ALL(z2):ALL(next2):[Set(n)

                             & 0 e n

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

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

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

                             & 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]]]

                             & Set(n')

                             & z2 e n'

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

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

                             & ALL(a):[a e n' => ~next2(a)=z2]

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

                             => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

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

                             & f(0)=z2

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

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

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

                                    U Spec, 35

 

                              37    ALL(next2):[Set(n)

                             & 0 e n

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

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

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

                             & 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]]]

                             & Set(n')

                             & 0' e n'

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

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

                             & ALL(a):[a e n' => ~next2(a)=0']

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

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

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

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

                             & f(0)=0'

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

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

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

                                    U Spec, 36

 

                              38    Set(n)

                             & 0 e n

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

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

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

                             & 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]]]

                             & Set(n')

                             & 0' e n'

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

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

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

                             & 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]]]

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

                             & f(0)=0'

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

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

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

                                    U Spec, 37

 

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

                            & f(0)=0'

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

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

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

                                    Detach, 38, 2

 

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

                             & f(0)=0'

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

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

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

                                    U Spec, 39

 

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

                             & f(0)=0'

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

                                    Join, 15, 18

 

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

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

                                    Detach, 40, 41

 

                        f is surjective

 

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

                                    Split, 42

 

                        f is injective

 

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

                                    Split, 42

 

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

                                    U Spec, 44

 

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

                                    U Spec, 45

 

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

                                    U Spec, 5

 

                              48    next(x) e n

                                    Detach, 47, 20

 

                              49    next(x) e n & y e n

                                    Join, 48, 21

 

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

                                    Detach, 46, 49

 

                              51    next(x)=y

                                    Detach, 50, 32

 

                   As Required:

 

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

                              4 Conclusion, 29

 

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

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

                              Join, 28, 52

 

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

                              Iff-And, 53

 

              As Required:

 

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

                        4 Conclusion, 19

 

          As Required:

 

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

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

                  4 Conclusion, 18

 

             

              '<='

             

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

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

             

              Suppose...

 

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

                        Premise

 

              Apply Subset Axiom for proof by induction

 

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

                        Subset, 3

 

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

                        E Spec, 58

 

              Define: p

 

                  60    Set(p)

                        Split, 59

 

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

                        Split, 59

 

              Apply PMI for n

 

                  62    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, 8

 

                  

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

                  

                   Suppose...

 

                        63    x e p

                              Premise

 

                   Apply defintion of p

 

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

                              U Spec, 61

 

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

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

                              Iff-And, 64

 

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

                              Split, 65

 

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

                              Split, 65

 

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

                              Detach, 66, 63

 

                        69    x e n

                              Split, 68

 

              As Required:

 

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

                        4 Conclusion, 63

 

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

                        Join, 60, 70

 

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

 

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

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

                        Detach, 62, 71

 

              BASE CASE

              *********

             

              Prove: 0 e p

             

              Apply definition of p

 

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

                        U Spec, 61

 

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

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

                        Iff-And, 73

 

                  75    0 e p => 0 e n & f(next(0))=next'(f(0))

                        Split, 74

 

              Sufficient: 0 e p

 

                  76    0 e n & f(next(0))=next'(f(0)) => 0 e p

                        Split, 74

 

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

                        U Spec, 57

 

                  78    0 e n & next(0) e n => [next(0)=next(0) <=> next'(f(0))=f(next(0))]

                        U Spec, 77

 

                  79    0 e n => next(0) e n

                        U Spec, 5

 

                  80    next(0) e n

                        Detach, 79, 4

 

                  81    0 e n & next(0) e n

                        Join, 4, 80

 

                  82    next(0)=next(0) <=> next'(f(0))=f(next(0))

                        Detach, 78, 81

 

                  83    [next(0)=next(0) => next'(f(0))=f(next(0))]

                   & [next'(f(0))=f(next(0)) => next(0)=next(0)]

                        Iff-And, 82

 

                  84    next(0)=next(0) => next'(f(0))=f(next(0))

                        Split, 83

 

                  85    next'(f(0))=f(next(0)) => next(0)=next(0)

                        Split, 83

 

                  86    next(0)=next(0)

                        Reflex

 

                  87    next'(f(0))=f(next(0))

                        Detach, 84, 86

 

                  88    f(next(0))=next'(f(0))

                        Sym, 87

 

                  89    0 e n & f(next(0))=next'(f(0))

                        Join, 4, 88

 

              As Required:

 

                  90    0 e p

                        Detach, 76, 89

 

                   INDUCTIVE STEP

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

                  

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

                  

                   Suppose...

 

                        91    x e p

                              Premise

 

                   Apply defintion of p

 

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

                              U Spec, 61

 

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

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

                              Iff-And, 92

 

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

                              Split, 93

 

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

                              Split, 93

 

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

                              Detach, 94, 91

 

                        97    x e n

                              Split, 96

 

                        98    f(next(x))=next'(f(x))

                              Split, 96

 

                   Apply definition of p

 

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

                              U Spec, 61

 

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

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

                              Iff-And, 99

 

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

                              Split, 100

 

                   Sufficient: For next(x) e p

 

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

                              Split, 100

 

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

                              U Spec, 5

 

                        104  next(x) e n

                              Detach, 103, 97

 

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

                              U Spec, 57

 

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

                              U Spec, 105

 

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

                              U Spec, 5

 

                        108  next(next(x)) e n

                              Detach, 107, 104

 

                        109  next(x) e n & next(next(x)) e n

                              Join, 104, 108

 

                        110  next(next(x))=next(next(x)) <=> next'(f(next(x)))=f(next(next(x)))

                              Detach, 106, 109

 

                        111  [next(next(x))=next(next(x)) => next'(f(next(x)))=f(next(next(x)))]

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

                              Iff-And, 110

 

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

                              Split, 111

 

                        113  next'(f(next(x)))=f(next(next(x))) => next(next(x))=next(next(x))

                              Split, 111

 

                        114  next(next(x))=next(next(x))

                              Reflex

 

                        115  next'(f(next(x)))=f(next(next(x)))

                              Detach, 112, 114

 

                        116  f(next(next(x)))=next'(f(next(x)))

                              Sym, 115

 

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

                              Join, 104, 116

 

                        118  next(x) e p

                              Detach, 102, 117

 

              As Required:

 

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

                        4 Conclusion, 91

 

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

                        Join, 90, 119

 

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

                        Detach, 72, 120

 

                  

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

                  

                   Suppose...

 

                        122  x e n

                              Premise

 

                        123  x e n => x e p

                              U Spec, 121

 

                        124  x e p

                              Detach, 123, 122

 

                   Apply definition of p

 

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

                              U Spec, 61

 

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

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

                              Iff-And, 125

 

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

                              Split, 126

 

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

                              Split, 126

 

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

                              Detach, 127, 124

 

                        130  x e n

                              Split, 129

 

                        131  f(next(x))=next'(f(x))

                              Split, 129

 

              As Required:

 

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

                        4 Conclusion, 122

 

          As Required:

 

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

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

                  4 Conclusion, 57

 

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

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

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

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

                  Join, 56, 133

 

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

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

                  Iff-And, 134

 

     As Required:

 

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

          & f(0)=0'

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

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

            4 Conclusion, 15

 

         

          '=>'

         

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

                 & f(0)=0'

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

         

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

                 & f(0)=0'

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

         

          Suppose...

 

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

              & f(0)=0'

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

                  Premise

 

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

                  Split, 137

 

            139  f(0)=0'

                  Split, 137

 

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

                  Split, 137

 

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

              & f(0)=0'

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

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

                  U Spec, 136

 

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

                  Join, 138, 139

 

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

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

                  Detach, 141, 142

 

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

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

                  Iff-And, 143

 

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

                  Split, 144

 

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

                  Split, 144

 

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

                  Detach, 145, 140

 

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

                  Join, 138, 139

 

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

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

                  Join, 148, 147

 

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

          & f(0)=0'

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

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

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

            4 Conclusion, 137

 

         

          '<='

         

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

                 & f(0)=0'

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

         

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

                 & f(0)=0'

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

         

          Suppose...

 

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

              & f(0)=0'

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

                  Premise

 

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

                  Split, 151

 

            153  f(0)=0'

                  Split, 151

 

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

                  Split, 151

 

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

              & f(0)=0'

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

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

                  U Spec, 136

 

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

                  Join, 152, 153

 

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

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

                  Detach, 155, 156

 

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

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

                  Iff-And, 157

 

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

                  Split, 158

 

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

                  Split, 158

 

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

                  Detach, 160, 154

 

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

                  Join, 152, 153

 

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

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

                  Join, 162, 161

 

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

          & f(0)=0'

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

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

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

            4 Conclusion, 151

 

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

          & f(0)=0'

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

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

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

          & f(0)=0'

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

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

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

            Join, 150, 164

 

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

          & f(0)=0'

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

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

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

            Iff-And, 165

 

Successor relations are preserved

 

As Required:

 

167  ALL(n1):ALL(z1):ALL(next1):ALL(n2):ALL(z2):ALL(next2):[Set(n1)

     & z1 e n1

     & ALL(a):[a e n1 => next1(a) e n1]

     & ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=next1(b) => a=b]]

     & ALL(a):[a e n1 => ~next1(a)=z1]

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

     => [z1 e a & ALL(b):[b e a => next1(b) e a]

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

     & Set(n2)

     & z2 e n2

     & ALL(a):[a e n2 => next2(a) e n2]

     & ALL(a):ALL(b):[a e n2 & b e n2 => [next2(a)=next2(b) => a=b]]

     & ALL(a):[a e n2 => ~next2(a)=z2]

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

     => [z2 e a & ALL(b):[b e a => next2(b) e a]

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

     => ALL(f):[ALL(a):[a e n1 => f(a) e n2]

     & f(z1)=z2

     & ALL(a):[a e n1 => f(next1(a))=next2(f(a))]

     <=> ALL(a):[a e n1 => f(a) e n2] & f(z1)=z2

     & ALL(a):ALL(b):[a e n1 & b e n1 => [next1(a)=b <=> next2(f(a))=f(b)]]]]

      4 Conclusion, 2