THEOREM

*******

 

There exists a unique exponent function on n with 0^0 left undefined.

 

Existence of exp(a,b):

 

   EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

   & exp(0,1)=0

   & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

   & ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]]

 

Uniqueness of exp(a,b):

 

   ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

   & exp(0,1)=0

   & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

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

   => [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

 

   & [ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

   & exp'(0,1)=0

   & ALL(a):[a e n => [~a=0 => exp'(a,0)=1]]

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

   => [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]

 

   => ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

 

 

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

Dan Christensen

2019-10-17

 

 

AXIOMS/DEFINITIONS

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

 

Define: n, 0, 1

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

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

4     ~1=0

      Axiom

 

5     0+1=1

      Axiom

 

 

Properties of +

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

 

Closed on n

 

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

      Axiom

 

Adding 0

 

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

      Axiom

 

+ Commutative

 

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

      Axiom

 

+ Right cancelable

 

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

      Axiom

 

0 is "first" number

 

10   ALL(a):[a e n => ~a+1=0]

      Axiom

 

Principle of Mathematical Induction

 

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

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

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

      Axiom

 

 

Properties of *

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

 

Closed on n

 

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

      Axiom

 

Multiplying by 0

 

13   ALL(a):[a e n => a*0=0]

      Axiom

 

Multiplying by 1

 

14   ALL(a):[a e n => a*1=a]

      Axiom

 

* Commutative

 

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

      Axiom

 

 

Function Axiom (2 varibles)

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

 

16   ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)

    => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]

    & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e f]]

    & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

    => [(a1,a2,b1) e f & (a1,a2,b2) e f => b1=b2]]

    => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=> (a1,a2,b) e f]]]]

      Function

 

PREVIOUS RESULT

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

 

There exists infinitely many exponent-like functions starting with exponent 0    Proof

 

17   ALL(x0):[x0 e n

    => EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

    & exp(0,0)=x0

    & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

    & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]]

      Axiom

 

   

    PROOF

*****

 

Suppose...

 

      18   x0 e n

            Premise

 

    Apply previous result

 

      19   x0 e n

         => EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]

            U Spec, 17

 

      20   EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]]

            Detach, 19, 18

 

      21   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

         & exp(0,0)=x0

         & ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

         & ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            E Spec, 20

 

   

    Define: exp

    ***********

 

      22   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

            Split, 21

 

      23   exp(0,0)=x0

            Split, 21

 

      24   ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

            Split, 21

 

      25   ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

            Split, 21

 

   

    Construct n2

 

      26   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

 

      27   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, 26

 

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

            U Spec, 27

 

      29   Set(n) & Set(n)

            Join, 1, 1

 

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

            Detach, 28, 29

 

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

            E Spec, 30

 

   

    Define: n2

 

      32   Set'(n2)

            Split, 31

 

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

            Split, 31

 

   

    Construct n3

 

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

            Cart Prod

 

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

            U Spec, 34

 

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

            U Spec, 35

 

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

            U Spec, 36

 

      38   Set(n) & Set(n)

            Join, 1, 1

 

      39   Set(n) & Set(n) & Set(n)

            Join, 38, 1

 

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

            Detach, 37, 39

 

      41   Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

            E Spec, 40

 

   

    Define: n3

 

      42   Set''(n3)

            Split, 41

 

      43   ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

            Split, 41

 

   

    Construct dom

 

      44   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & ~[a=0 & b=0]]]

            Subset, 32

 

      45   Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]

            E Spec, 44

 

   

    Define: dom

 

      46   Set'(dom)

            Split, 45

 

      47   ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & ~[a=0 & b=0]]

            Split, 45

 

   

    Construct exp'

 

      48   EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

         <=> (a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]]

            Subset, 42

 

      49   Set''(exp') & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'

         <=> (a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]

            E Spec, 48

 

   

    Define: exp'

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

 

      50   Set''(exp')

            Split, 49

 

      51   ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'

         <=> (a,b,c) e n3 & [~[a=0 & b=0] & c=exp(a,b)]]

            Split, 49

 

   

    Apply Function Axioms (for 2 variables)

 

      52   ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e f]]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

         => [(a1,a2,b1) e f & (a1,a2,b2) e f => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=> (a1,a2,b) e f]]]]

            Function

 

      53   ALL(dom):ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e exp']]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]]

            U Spec, 52

 

      54   ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e exp']]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]]

            U Spec, 53

 

      55   Set''(exp') & Set'(dom) & Set(n)

         => [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]

            U Spec, 54

 

      56   Set''(exp') & Set'(dom)

            Join, 50, 46

 

      57   Set''(exp') & Set'(dom) & Set(n)

            Join, 56, 1

 

   

    Sufficient: For functionality of exp'

 

      58   ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

         => ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]

            Detach, 55, 57

 

        

         Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

        

         Suppose...

 

            59   (x,y,z) e exp'

                  Premise

 

         Apply definition of exp'

 

            60   ALL(b):ALL(c):[(x,b,c) e exp'

             <=> (x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]

                  U Spec, 51

 

            61   ALL(c):[(x,y,c) e exp'

             <=> (x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]

                  U Spec, 60

 

            62   (x,y,z) e exp'

             <=> (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                  U Spec, 61

 

            63   [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]

             & [(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']

                  Iff-And, 62

 

            64   (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                  Split, 63

 

            65   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'

                  Split, 63

 

            66   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

                  Detach, 64, 59

 

            67   (x,y,z) e n3

                  Split, 66

 

            68   ~[x=0 & y=0] & z=exp(x,y)

                  Split, 66

 

            69   ~[x=0 & y=0]

                  Split, 68

 

            70   z=exp(x,y)

                  Split, 68

 

            71   ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                  U Spec, 47

 

            72   (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                  U Spec, 71

 

            73   [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

             & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                  Iff-And, 72

 

            74   (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                  Split, 73

 

         Apply definition of n3

 

            75   ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 43

 

            76   ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

                  U Spec, 75

 

            77   (x,y,z) e n3 <=> x e n & y e n & z e n

                  U Spec, 76

 

            78   [(x,y,z) e n3 => x e n & y e n & z e n]

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

                  Iff-And, 77

 

            79   (x,y,z) e n3 => x e n & y e n & z e n

                  Split, 78

 

            80   x e n & y e n & z e n => (x,y,z) e n3

                  Split, 78

 

            81   x e n & y e n & z e n

                  Detach, 79, 67

 

            82   x e n

                  Split, 81

 

            83   y e n

                  Split, 81

 

            84   z e n

                  Split, 81

 

         Sufficient: For (x,y) e dom

 

            85   (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                  Split, 73

 

         Apply definition of n3

 

            86   ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 43

 

            87   ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

                  U Spec, 86

 

            88   (x,y,z) e n3 <=> x e n & y e n & z e n

                  U Spec, 87

 

            89   [(x,y,z) e n3 => x e n & y e n & z e n]

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

                  Iff-And, 88

 

            90   (x,y,z) e n3 => x e n & y e n & z e n

                  Split, 89

 

            91   x e n & y e n & z e n => (x,y,z) e n3

                  Split, 89

 

            92   x e n & y e n & z e n

                  Detach, 90, 67

 

            93   x e n

                  Split, 92

 

            94   y e n

                  Split, 92

 

            95   z e n

                  Split, 92

 

         Apply definition of n2

 

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

                  U Spec, 33

 

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

                  U Spec, 96

 

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

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

                  Iff-And, 97

 

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

                  Split, 98

 

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

                  Split, 98

 

            101  x e n & y e n

                  Join, 82, 83

 

            102  (x,y) e n2

                  Detach, 100, 101

 

            103  (x,y) e n2 & ~[x=0 & y=0]

                  Join, 102, 69

 

            104  (x,y) e dom

                  Detach, 85, 103

 

            105  (x,y) e dom & z e n

                  Join, 104, 84

 

    Functionality of exp', Part 1

 

      106  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

            4 Conclusion, 59

 

        

         Prove: ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

        

         Suppose...

 

            107  (x,y) e dom

                  Premise

 

         Apply definition of dom

 

            108  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                  U Spec, 47

 

            109  (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                  U Spec, 108

 

            110  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

             & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                  Iff-And, 109

 

            111  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                  Split, 110

 

            112  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                  Split, 110

 

            113  (x,y) e n2 & ~[x=0 & y=0]

                  Detach, 111, 107

 

            114  (x,y) e n2

                  Split, 113

 

            115  ~[x=0 & y=0]

                  Split, 113

 

         Apply definition of exp'

 

            116  ALL(b):ALL(c):[(x,b,c) e exp'

             <=> (x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]

                  U Spec, 51

 

            117  ALL(c):[(x,y,c) e exp'

             <=> (x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]

                  U Spec, 116

 

            118  ALL(b):[x e n & b e n => exp(x,b) e n]

                  U Spec, 22

 

            119  x e n & y e n => exp(x,y) e n

                  U Spec, 118

 

         Apply definition of n2

 

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

                  U Spec, 33

 

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

                  U Spec, 120

 

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

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

                  Iff-And, 121

 

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

                  Split, 122

 

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

                  Split, 122

 

            125  x e n & y e n

                  Detach, 123, 114

 

            126  x e n

                  Split, 125

 

            127  y e n

                  Split, 125

 

            128  exp(x,y) e n

                  Detach, 119, 125

 

            129  (x,y,exp(x,y)) e exp'

             <=> (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  U Spec, 117, 128

 

            130  [(x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]]

             & [(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp']

                  Iff-And, 129

 

            131  (x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  Split, 130

 

         Sufficient: For (x,y,exp(x,y)) e exp'

 

            132  (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp'

                  Split, 130

 

         Apply definition of n3

 

            133  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 43

 

            134  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

                  U Spec, 133

 

            135  (x,y,exp(x,y)) e n3 <=> x e n & y e n & exp(x,y) e n

                  U Spec, 134, 128

 

            136  [(x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n]

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

                  Iff-And, 135

 

            137  (x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n

                  Split, 136

 

         Sufficient: For (x,y,exp(x,y)) e n3

 

            138  x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3

                  Split, 136

 

            139  x e n & y e n & exp(x,y) e n

                  Join, 125, 128

 

            140  (x,y,exp(x,y)) e n3

                  Detach, 138, 139

 

            141  exp(x,y)=exp(x,y)

                  Reflex, 128

 

            142  ~[x=0 & y=0] & exp(x,y)=exp(x,y)

                  Join, 115, 141

 

            143  (x,y,exp(x,y)) e n3

             & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

                  Join, 140, 142

 

            144  (x,y,exp(x,y)) e exp'

                  Detach, 132, 143

 

            145  exp(x,y) e n & (x,y,exp(x,y)) e exp'

                  Join, 128, 144

 

            146  EXIST(b):[b e n & (x,y,b) e exp']

                  E Gen, 145

 

    Functionality of exp', Part 2

 

      147  ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

            4 Conclusion, 107

 

        

         Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

                => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

        

         Suppose...

 

            148  (x,y) e dom & z1 e n & z2 e n

                  Premise

 

            149  (x,y) e dom

                  Split, 148

 

            150  z1 e n

                  Split, 148

 

            151  z2 e n

                  Split, 148

 

            

             Suppose...

 

                  152  (x,y,z1) e exp' & (x,y,z2) e exp'

                        Premise

 

                  153  (x,y,z1) e exp'

                        Split, 152

 

                  154  (x,y,z2) e exp'

                        Split, 152

 

             Apply the definition of exp'

 

                  155  ALL(b):ALL(c):[(x,b,c) e exp'

                 <=> (x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]

                        U Spec, 51

 

                  156  ALL(c):[(x,y,c) e exp'

                 <=> (x,y,c) e n3 & [~[x=0 & y=0] & c=exp(x,y)]]

                        U Spec, 155

 

                  157  (x,y,z1) e exp'

                 <=> (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        U Spec, 156

 

                  158  [(x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]]

                 & [(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp']

                        Iff-And, 157

 

                  159  (x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        Split, 158

 

                  160  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp'

                        Split, 158

 

                  161  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

                        Detach, 159, 153

 

                  162  (x,y,z1) e n3

                        Split, 161

 

                  163  ~[x=0 & y=0] & z1=exp(x,y)

                        Split, 161

 

                  164  ~[x=0 & y=0]

                        Split, 163

 

                  165  z1=exp(x,y)

                        Split, 163

 

                  166  (x,y,z2) e exp'

                 <=> (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        U Spec, 156

 

                  167  [(x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]]

                 & [(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp']

                        Iff-And, 166

 

                  168  (x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        Split, 167

 

                  169  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp'

                        Split, 167

 

                  170  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

                        Detach, 168, 154

 

                  171  (x,y,z2) e n3

                        Split, 170

 

                  172  ~[x=0 & y=0] & z2=exp(x,y)

                        Split, 170

 

                  173  ~[x=0 & y=0]

                        Split, 172

 

                  174  z2=exp(x,y)

                        Split, 172

 

                  175  z1=z2

                        Substitute, 174, 165

 

            176  (x,y,z1) e exp' & (x,y,z2) e exp' => z1=z2

                  4 Conclusion, 152

 

    Functionality of exp', Part 3

 

      177  ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

            4 Conclusion, 148

 

    Joining results...

 

      178  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

            Join, 106, 147

 

      179  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

         & ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

         & ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

         => [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

            Join, 178, 177

 

   

    exp' is a partial binary function on n

   

    As Required:

 

      180  ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]

            Detach, 58, 179

 

        

         Prove: ALL(x):ALL(y):[x e n & y e n => [~[x=0 & y=0] => exp'(x,y) e n]]

        

         Suppose...

 

            181  x e n & y e n

                  Premise

 

            

             Prove: ~[x=0 & y=0] => exp'(x,y) e n

            

             Suppose...

 

                  182  ~[x=0 & y=0]

                        Premise

 

             Apply definition of exp'

 

                  183  ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]

                        U Spec, 147

 

                  184  (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']

                        U Spec, 183

 

             Apply definition of dom

 

                  185  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  186  (x,y) e dom <=> (x,y) e n2 & ~[x=0 & y=0]

                        U Spec, 185

 

                  187  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

                 & [(x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom]

                        Iff-And, 186

 

                  188  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

                        Split, 187

 

                  189  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

                        Split, 187

 

             Apply definition of n2

 

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

                        U Spec, 33

 

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

                        U Spec, 190

 

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

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

                        Iff-And, 191

 

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

                        Split, 192

 

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

                        Split, 192

 

                  195  (x,y) e n2

                        Detach, 194, 181

 

                  196  (x,y) e n2 & ~[x=0 & y=0]

                        Join, 195, 182

 

                  197  (x,y) e dom

                        Detach, 189, 196

 

                  198  EXIST(b):[b e n & (x,y,b) e exp']

                        Detach, 184, 197

 

                  199  z e n & (x,y,z) e exp'

                        E Spec, 198

 

                  200  z e n

                        Split, 199

 

                  201  (x,y,z) e exp'

                        Split, 199

 

             Apply previous result

 

                  202  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  203  ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]

                        U Spec, 202

 

                  204  (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']

                        U Spec, 203

 

                  205  (x,y) e dom & z e n

                        Join, 197, 200

 

                  206  exp'(x,y)=z <=> (x,y,z) e exp'

                        Detach, 204, 205

 

                  207  [exp'(x,y)=z => (x,y,z) e exp']

                 & [(x,y,z) e exp' => exp'(x,y)=z]

                        Iff-And, 206

 

                  208  exp'(x,y)=z => (x,y,z) e exp'

                        Split, 207

 

                  209  (x,y,z) e exp' => exp'(x,y)=z

                        Split, 207

 

                  210  exp'(x,y)=z

                        Detach, 209, 201

 

                  211  exp'(x,y) e n

                        Substitute, 210, 200

 

         As Required:

 

            212  ~[x=0 & y=0] => exp'(x,y) e n

                  4 Conclusion, 182

 

   

    As Required:

 

      213  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

            4 Conclusion, 181

 

   

    Prove: exp'(0,1)=0

   

    Apply definition of exp'

 

      214  ALL(b):ALL(c):[(0,b,c) e exp'

         <=> (0,b,c) e n3 & [~[0=0 & b=0] & c=exp(0,b)]]

            U Spec, 51

 

      215  ALL(c):[(0,1,c) e exp'

         <=> (0,1,c) e n3 & [~[0=0 & 1=0] & c=exp(0,1)]]

            U Spec, 214

 

      216  (0,1,0) e exp'

         <=> (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

            U Spec, 215

 

      217  [(0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]]

         & [(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp']

            Iff-And, 216

 

      218  (0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

            Split, 217

 

    Sufficient: For (0,1,0) e exp'

 

      219  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp'

            Split, 217

 

    Apply definition of n3

 

      220  ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]

            U Spec, 43

 

      221  ALL(c3):[(0,1,c3) e n3 <=> 0 e n & 1 e n & c3 e n]

            U Spec, 220

 

      222  (0,1,0) e n3 <=> 0 e n & 1 e n & 0 e n

            U Spec, 221

 

      223  [(0,1,0) e n3 => 0 e n & 1 e n & 0 e n]

         & [0 e n & 1 e n & 0 e n => (0,1,0) e n3]

            Iff-And, 222

 

      224  (0,1,0) e n3 => 0 e n & 1 e n & 0 e n

            Split, 223

 

      225  0 e n & 1 e n & 0 e n => (0,1,0) e n3

            Split, 223

 

      226  0 e n & 1 e n

            Join, 2, 3

 

      227  0 e n & 1 e n & 0 e n

            Join, 226, 2

 

      228  (0,1,0) e n3

            Detach, 225, 227

 

        

         Prove: ~[0=0 & 1=0]

        

         Suppose to the contrary...

 

            229  0=0 & 1=0

                  Premise

 

            230  0=0

                  Split, 229

 

            231  1=0

                  Split, 229

 

            232  1=0 & ~1=0

                  Join, 231, 4

 

      233  ~[0=0 & 1=0]

            4 Conclusion, 229

 

    Apply definition of exp

 

      234  ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]

            U Spec, 25

 

      235  0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0

            U Spec, 234

 

      236  0 e n & 0 e n

            Join, 2, 2

 

      237  exp(0,0+1)=exp(0,0)*0

            Detach, 235, 236

 

      238  ALL(b):[0 e n & b e n => 0+b=b+0]

            U Spec, 8

 

      239  0 e n & 1 e n => 0+1=1+0

            U Spec, 238

 

      240  0 e n & 1 e n

            Join, 2, 3

 

      241  0+1=1+0

            Detach, 239, 240

 

      242  1 e n => 1+0=1

            U Spec, 7

 

      243  1+0=1

            Detach, 242, 3

 

      244  0+1=1

            Substitute, 243, 241

 

      245  exp(0,1)=exp(0,0)*0

            Substitute, 244, 237

 

      246  ALL(b):[0 e n & b e n => exp(0,b) e n]

            U Spec, 22

 

      247  0 e n & 0 e n => exp(0,0) e n

            U Spec, 246

 

      248  0 e n & 0 e n

            Join, 2, 2

 

      249  exp(0,0) e n

            Detach, 247, 248

 

      250  exp(0,0) e n => exp(0,0)*0=0

            U Spec, 13, 249

 

      251  exp(0,0)*0=0

            Detach, 250, 249

 

      252  exp(0,1)=0

            Substitute, 251, 245

 

      253  0=exp(0,1)

            Sym, 252

 

      254  ~[0=0 & 1=0] & 0=exp(0,1)

            Join, 233, 253

 

      255  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

            Join, 228, 254

 

      256  (0,1,0) e exp'

            Detach, 219, 255

 

    Apply previous result

 

      257  ALL(a2):ALL(b):[(0,a2) e dom & b e n => [exp'(0,a2)=b <=> (0,a2,b) e exp']]

            U Spec, 180

 

      258  ALL(b):[(0,1) e dom & b e n => [exp'(0,1)=b <=> (0,1,b) e exp']]

            U Spec, 257

 

      259  (0,1) e dom & 0 e n => [exp'(0,1)=0 <=> (0,1,0) e exp']

            U Spec, 258

 

    Apply defintion of dom

 

      260  ALL(b):[(0,b) e dom <=> (0,b) e n2 & ~[0=0 & b=0]]

            U Spec, 47

 

      261  (0,1) e dom <=> (0,1) e n2 & ~[0=0 & 1=0]

            U Spec, 260

 

      262  [(0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]]

         & [(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom]

            Iff-And, 261

 

      263  (0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]

            Split, 262

 

      264  (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom

            Split, 262

 

      265  ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]

            U Spec, 33

 

      266  (0,1) e n2 <=> 0 e n & 1 e n

            U Spec, 265

 

      267  [(0,1) e n2 => 0 e n & 1 e n]

         & [0 e n & 1 e n => (0,1) e n2]

            Iff-And, 266

 

      268  (0,1) e n2 => 0 e n & 1 e n

            Split, 267

 

      269  0 e n & 1 e n => (0,1) e n2

            Split, 267

 

      270  0 e n & 1 e n

            Join, 2, 3

 

      271  (0,1) e n2

            Detach, 269, 270

 

            272  0=0 & 1=0

                  Premise

 

            273  0=0

                  Split, 272

 

            274  1=0

                  Split, 272

 

            275  1=0 & ~1=0

                  Join, 274, 4

 

      276  ~[0=0 & 1=0]

            4 Conclusion, 272

 

      277  (0,1) e n2 & ~[0=0 & 1=0]

            Join, 271, 276

 

      278  (0,1) e dom

            Detach, 264, 277

 

      279  (0,1) e dom & 0 e n

            Join, 278, 2

 

      280  exp'(0,1)=0 <=> (0,1,0) e exp'

            Detach, 259, 279

 

      281  [exp'(0,1)=0 => (0,1,0) e exp']

         & [(0,1,0) e exp' => exp'(0,1)=0]

            Iff-And, 280

 

      282  exp'(0,1)=0 => (0,1,0) e exp'

            Split, 281

 

      283  (0,1,0) e exp' => exp'(0,1)=0

            Split, 281

 

   

    As Required:

 

      284  exp'(0,1)=0

            Detach, 283, 256

 

        

         Prove: ALL(a):[a e n => [~x=0 => exp'(x,0)=1]]

        

         Suppose...

 

            285  x e n

                  Premise

 

            

             Prove: ~x=0 => exp'(x,0)=1

            

             Suppose...

 

                  286  ~x=0

                        Premise

 

                  287  ALL(b):ALL(c):[(x,b,c) e exp'

                 <=> (x,b,c) e n3 & [~[x=0 & b=0] & c=exp(x,b)]]

                        U Spec, 51

 

                  288  ALL(c):[(x,0,c) e exp'

                 <=> (x,0,c) e n3 & [~[x=0 & 0=0] & c=exp(x,0)]]

                        U Spec, 287

 

                  289  (x,0,1) e exp'

                 <=> (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

                        U Spec, 288

 

                  290  [(x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]]

                 & [(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp']

                        Iff-And, 289

 

                  291  (x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

                        Split, 290

 

             Sufficient: For (x,0,1) e exp'

 

                  292  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp'

                        Split, 290

 

             Apply definition of n3

 

                  293  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                        U Spec, 43

 

                  294  ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]

                        U Spec, 293

 

                  295  (x,0,1) e n3 <=> x e n & 0 e n & 1 e n

                        U Spec, 294

 

                  296  [(x,0,1) e n3 => x e n & 0 e n & 1 e n]

                 & [x e n & 0 e n & 1 e n => (x,0,1) e n3]

                        Iff-And, 295

 

                  297  [(x,0,1) e n3 => x e n & 0 e n & 1 e n]

                 & [x e n & 0 e n & 1 e n => (x,0,1) e n3]

                        Iff-And, 295

 

                  298  (x,0,1) e n3 => x e n & 0 e n & 1 e n

                        Split, 297

 

                  299  x e n & 0 e n & 1 e n => (x,0,1) e n3

                        Split, 297

 

                  300  x e n & 0 e n

                        Join, 285, 2

 

                  301  x e n & 0 e n & 1 e n

                        Join, 300, 3

 

                  302  (x,0,1) e n3

                        Detach, 299, 301

 

                        303  x=0 & 0=0

                              Premise

 

                        304  x=0

                              Split, 303

 

                        305  0=0

                              Split, 303

 

                        306  x=0 & ~x=0

                              Join, 304, 286

 

                  307  ~[x=0 & 0=0]

                        4 Conclusion, 303

 

             Apply definition of exp

 

                  308  x e n => [~x=0 => exp(x,0)=1]

                        U Spec, 24

 

                  309  ~x=0 => exp(x,0)=1

                        Detach, 308, 285

 

                  310  exp(x,0)=1

                        Detach, 309, 286

 

                  311  1=exp(x,0)

                        Sym, 310

 

                  312  ~[x=0 & 0=0] & 1=exp(x,0)

                        Join, 307, 311

 

                  313  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

                        Join, 302, 312

 

                  314  (x,0,1) e exp'

                        Detach, 292, 313

 

                  315  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

                        U Spec, 180

 

                  316  ALL(b):[(x,0) e dom & b e n => [exp'(x,0)=b <=> (x,0,b) e exp']]

                        U Spec, 315

 

                  317  (x,0) e dom & 1 e n => [exp'(x,0)=1 <=> (x,0,1) e exp']

                        U Spec, 316

 

             Apply definition of dom

 

                  318  ALL(b):[(x,b) e dom <=> (x,b) e n2 & ~[x=0 & b=0]]

                        U Spec, 47

 

                  319  (x,0) e dom <=> (x,0) e n2 & ~[x=0 & 0=0]

                        U Spec, 318

 

                  320  [(x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]]

                 & [(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom]

                        Iff-And, 319

 

                  321  (x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]

                        Split, 320

 

                  322  (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom

                        Split, 320

 

             Apply definition of n2

 

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

                        U Spec, 33

 

                  324  (x,0) e n2 <=> x e n & 0 e n

                        U Spec, 323

 

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

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

                        Iff-And, 324

 

                  326  (x,0) e n2 => x e n & 0 e n

                        Split, 325

 

                  327  x e n & 0 e n => (x,0) e n2

                        Split, 325

 

                  328  x e n & 0 e n

                        Join, 285, 2

 

                  329  (x,0) e n2

                        Detach, 327, 328

 

                        330  x=0 & 0=0

                              Premise

 

                        331  x=0

                              Split, 330

 

                        332  0=0

                              Split, 330

 

                        333  x=0 & ~x=0

                              Join, 331, 286

 

                  334  ~[x=0 & 0=0]

                        4 Conclusion, 330

 

                  335  (x,0) e n2 & ~[x=0 & 0=0]

                        Join, 329, 334

 

                  336  (x,0) e dom

                        Detach, 322, 335

 

                  337  (x,0) e dom & 1 e n

                        Join, 336, 3

 

                  338  exp'(x,0)=1 <=> (x,0,1