THEOREM

*******

Recall that there are infinitely many exponent-like functions ^ on the natural numbers such that:

1. x^2 = x*x

2. x^(y+1) = x^y * x

See proof

Here, we will show that these infinitely many functions will differ ONLY in the value assigned to 0^0, i.e. they will

yield the SAME result for x^y if we do NOT have x = y = 0.

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

OUTLINE

*******

Lines    Content

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

1-7      Axioms/Definition

8        Previous result (link to proof)

9-13     Define exponent-like functions exp1 and exp2 that start by defining powers of 2

14-30    Convert exp1 and exp2 to equivalent functions that start by defining powers of 0

31-194   Prove by induction that if ~[x=0 & y=0] then exp1(x,y)=exp2(x,y)

AXIOMS/DEFINITIONS

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

Define: n, 0, 1, 2

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

1     Set(n)

Axiom

2     0 e n

Axiom

3     1 e n

Axiom

Properties of +

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

Closed on n

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

Axiom

Principle of mathematical deduction using addition on n

5     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

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

Axiom

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

Axiom

PREVIOUS RESULT

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

In the context of exponent-like functions, starting by defining powers of 2 is equivalent to starting

by defining powers of 0                                                                                     Proof

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

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

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

<=> ALL(a):[a e n => exp(a,2)=a*a]]]]

Axiom

PROOF

*****

Suppose...

9     ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

& ALL(a):[a e n => exp1(a,2)=a*a]

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

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

& ALL(a):[a e n => exp2(a,2)=a*a]

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

Premise

Define: exp1

10   ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

Split, 9

11   ALL(a):[a e n => exp1(a,2)=a*a]

Split, 9

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

Split, 9

13   ALL(a):ALL(b):[a e n & b e n => exp2(a,b) e n]

& ALL(a):[a e n => exp2(a,2)=a*a]

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

Split, 9

Define: exp2

14   ALL(a):ALL(b):[a e n & b e n => exp2(a,b) e n]

Split, 13

15   ALL(a):[a e n => exp2(a,2)=a*a]

Split, 13

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

Split, 13

Apply previous result for exp1

17   ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

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

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

<=> ALL(a):[a e n => exp1(a,2)=a*a]]]

U Spec, 8

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

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

<=> ALL(a):[a e n => exp1(a,2)=a*a]]

Detach, 17, 10

19   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

<=> ALL(a):[a e n => exp1(a,2)=a*a]

Detach, 18, 12

20   [ALL(a):[a e n => [~a=0 => exp1(a,0)=1]] => ALL(a):[a e n => exp1(a,2)=a*a]]

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

Iff-And, 19

21   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]] => ALL(a):[a e n => exp1(a,2)=a*a]

Split, 20

22   ALL(a):[a e n => exp1(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

Split, 20

23   ALL(a):[a e n => [~a=0 => exp1(a,0)=1]]

Detach, 22, 11

Apply previous result for exp2

24   ALL(a):ALL(b):[a e n & b e n => exp2(a,b) e n]

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

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

<=> ALL(a):[a e n => exp2(a,2)=a*a]]]

U Spec, 8

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

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

<=> ALL(a):[a e n => exp2(a,2)=a*a]]

Detach, 24, 14

26   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

<=> ALL(a):[a e n => exp2(a,2)=a*a]

Detach, 25, 16

27   [ALL(a):[a e n => [~a=0 => exp2(a,0)=1]] => ALL(a):[a e n => exp2(a,2)=a*a]]

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

Iff-And, 26

28   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]] => ALL(a):[a e n => exp2(a,2)=a*a]

Split, 27

29   ALL(a):[a e n => exp2(a,2)=a*a] => ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

Split, 27

30   ALL(a):[a e n => [~a=0 => exp2(a,0)=1]]

Detach, 29, 15

Prove: ALL(a):[a e n

=> ALL(b):[b e n => [~[a=0 & b=0] => exp1(a,b)=exp2(a,b)]]]  (by induction)

Suppose...

31   x e n

Premise

Construct set p for proof by induction

32   EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]]

Subset, 1

33   Set(p) & ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

E Spec, 32

Define: p

34   Set(p)

Split, 33

35   ALL(b):[b e p <=> b e n & [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

Split, 33

Apply principle of induction

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

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

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

U Spec, 5

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

Suppose...

37   y e p

Premise

38   y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

U Spec, 35

39   [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

& [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

Iff-And, 38

40   y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Split, 39

41   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

Split, 39

42   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Detach, 40, 37

43   y e n

Split, 42

As Required:

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

4 Conclusion, 37

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

Join, 34, 44

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

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

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

Detach, 36, 45

BASE CASE

*********

Apply definition p

47   0 e p <=> 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

U Spec, 35

48   [0 e p => 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]]

& [0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)] => 0 e p]

Iff-And, 47

49   0 e p => 0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

Split, 48

Sufficient: For 0 e p

50   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)] => 0 e p

Split, 48

Two cases to consider:

51   x=0 | ~x=0

Or Not

Case 1

Prove: x=0 => 0 e p

Suppose...

52   x=0

Premise

53   0=0

Reflex

54   x=0 & 0=0

Join, 52, 53

Prove: ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

Suppose...

55   ~[x=0 & 0=0]

Premise

56   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

Arb Cons, 54

57   exp1(x,0)=exp2(x,0)

Detach, 56, 55

As Required:

58   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

4 Conclusion, 55

59   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

Join, 2, 58

60   0 e p

Detach, 50, 59

Case 1

As Required:

61   x=0 => 0 e p

4 Conclusion, 52

Case 2

Prove: ~x=0 => 0 e p

Suppose...

62   ~x=0

Premise

Prove: ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

Suppose...

63   ~[x=0 & 0=0]

Premise

64   x e n => [~x=0 => exp1(x,0)=1]

U Spec, 23

65   ~x=0 => exp1(x,0)=1

Detach, 64, 31

66   exp1(x,0)=1

Detach, 65, 62

67   x e n => [~x=0 => exp2(x,0)=1]

U Spec, 30

68   ~x=0 => exp2(x,0)=1

Detach, 67, 31

69   exp2(x,0)=1

Detach, 68, 62

70   exp1(x,0)=exp2(x,0)

Substitute, 69, 66

As Required:

71   ~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)

4 Conclusion, 63

72   0 e n & [~[x=0 & 0=0] => exp1(x,0)=exp2(x,0)]

Join, 2, 71

73   0 e p

Detach, 50, 72

Case 2

As Required:

74   ~x=0 => 0 e p

4 Conclusion, 62

75   [x=0 => 0 e p] & [~x=0 => 0 e p]

Join, 61, 74

As Required:

76   0 e p

Cases, 51, 75

INDUCTIVE STEP

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

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

Suppose...

77   y e p

Premise

Apply definition of p

78   y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

U Spec, 35

79   [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

& [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

Iff-And, 78

80   y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Split, 79

81   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

Split, 79

82   y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Detach, 80, 77

83   y e n

Split, 82

84   ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

Split, 82

Apply axiom

85   ALL(b):[y e n & b e n => y+b e n]

U Spec, 4

86   y e n & 1 e n => y+1 e n

U Spec, 85

87   y e n & 1 e n

Join, 83, 3

88   y+1 e n

Detach, 86, 87

Apply definition of p

89   y+1 e p <=> y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]

U Spec, 35, 88

90   [y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]]

& [y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)] => y+1 e p]

Iff-And, 89

91   y+1 e p => y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)]

Split, 90

Sufficient: For y+1 e p

92   y+1 e n & [~[x=0 & y+1=0] => exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

Split, 90

93   y+1 e n & [~~[x=0 & y+1=0] | exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

Imply-Or, 92

94   y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)] => y+1 e p

Rem DNeg, 93

Case 1

Prove: x=0 => y+1 e p

Suppose...

95   x=0

Premise

Two sub-cases to consider:

96   y=0 | ~y=0

Or Not

Sub-case 1

Prove: y=0 => y+1 e p

Suppose...

97   y=0

Premise

Apply definition of exp1

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

U Spec, 12

99   0 e n & 0 e n => exp1(0,0+1)=exp1(0,0)*0

U Spec, 98

100  0 e n & 0 e n

Join, 2, 2

101  exp1(0,0+1)=exp1(0,0)*0

Detach, 99, 100

Apply definition of exp1

102  ALL(b):[0 e n & b e n => exp1(0,b) e n]

U Spec, 10

103  0 e n & 0 e n => exp1(0,0) e n

U Spec, 102

104  0 e n & 0 e n

Join, 2, 2

105  exp1(0,0) e n

Detach, 103, 104

Apply axiom

106  exp1(0,0) e n => exp1(0,0)*0=0

U Spec, 7, 105

107  exp1(0,0)*0=0

Detach, 106, 105

108  exp1(0,0+1)=0

Substitute, 107, 101

Apply definition of exp2

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

U Spec, 16

110  0 e n & 0 e n => exp2(0,0+1)=exp2(0,0)*0

U Spec, 109

111  exp2(0,0+1)=exp2(0,0)*0

Detach, 110, 104

Apply definition of exp2

112  ALL(b):[0 e n & b e n => exp2(0,b) e n]

U Spec, 14

113  0 e n & 0 e n => exp2(0,0) e n

U Spec, 112

114  exp2(0,0) e n

Detach, 113, 104

Apply axiom

115  exp2(0,0) e n => exp2(0,0)*0=0

U Spec, 7, 114

116  exp2(0,0)*0=0

Detach, 115, 114

117  exp2(0,0+1)=0

Substitute, 116, 111

118  exp1(0,0+1)=exp2(0,0+1)

Substitute, 117, 108

119  exp1(x,0+1)=exp2(x,0+1)

Substitute, 95, 118

120  exp1(x,y+1)=exp2(x,y+1)

Substitute, 97, 119

121  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

Arb Or, 120

122  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

Join, 88, 121

123  y+1 e p

Detach, 94, 122

Sub-case 1

As Required:

124  y=0 => y+1 e p

4 Conclusion, 97

Sub-case 2

Prove: ~y=0 => y+1 e p

Suppose...

125  ~y=0

Premise

Prove: ~y=0 => y+1 e p

Suppose to the contrary...

126  x=0 & y=0

Premise

127  x=0

Split, 126

128  y=0

Split, 126

129  y=0 & ~y=0

Join, 128, 125

As Required:

130  ~[x=0 & y=0]

4 Conclusion, 126

131  exp1(x,y)=exp2(x,y)

Detach, 84, 130

Apply definition of exp1

132  ALL(b):[x e n & b e n => exp1(x,b+1)=exp1(x,b)*x]

U Spec, 12

133  x e n & y e n => exp1(x,y+1)=exp1(x,y)*x

U Spec, 132

134  x e n & y e n

Join, 31, 83

135  exp1(x,y+1)=exp1(x,y)*x

Detach, 133, 134

Apply definition of exp2

136  ALL(b):[x e n & b e n => exp2(x,b+1)=exp2(x,b)*x]

U Spec, 16

137  x e n & y e n => exp2(x,y+1)=exp2(x,y)*x

U Spec, 136

138  exp2(x,y+1)=exp2(x,y)*x

Detach, 137, 134

139  exp2(x,y+1)=exp1(x,y)*x

Substitute, 131, 138

140  exp1(x,y+1)=exp2(x,y+1)

Substitute, 139, 135

141  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

Arb Or, 140

142  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

Join, 88, 141

143  y+1 e p

Detach, 94, 142

Sub-case 2

As Required:

144  ~y=0 => y+1 e p

4 Conclusion, 125

145  [y=0 => y+1 e p] & [~y=0 => y+1 e p]

Join, 124, 144

146  y+1 e p

Cases, 96, 145

Case 1

As Required:

147  x=0 => y+1 e p

4 Conclusion, 95

Case 2

Prove: ~x=0 => y+1 e p

Suppose...

148  ~x=0

Premise

Prove: ~[x=0 & y=0]

Suppose to the contrary...

149  x=0 & y=0

Premise

150  x=0

Split, 149

151  y=0

Split, 149

152  x=0 & ~x=0

Join, 150, 148

As Required:

153  ~[x=0 & y=0]

4 Conclusion, 149

154  exp1(x,y)=exp2(x,y)

Detach, 84, 153

Apply definition of exp1

155  ALL(b):[x e n & b e n => exp1(x,b+1)=exp1(x,b)*x]

U Spec, 12

156  x e n & y e n => exp1(x,y+1)=exp1(x,y)*x

U Spec, 155

157  x e n & y e n

Join, 31, 83

158  exp1(x,y+1)=exp1(x,y)*x

Detach, 156, 157

Apply definition of exp2

159  ALL(b):[x e n & b e n => exp2(x,b+1)=exp2(x,b)*x]

U Spec, 16

160  x e n & y e n => exp2(x,y+1)=exp2(x,y)*x

U Spec, 159

161  x e n & y e n

Join, 31, 83

162  exp2(x,y+1)=exp2(x,y)*x

Detach, 160, 161

163  exp2(x,y+1)=exp1(x,y)*x

Substitute, 154, 162

164  exp1(x,y+1)=exp2(x,y+1)

Substitute, 163, 158

165  x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)

Arb Or, 164

166  y+1 e n & [x=0 & y+1=0 | exp1(x,y+1)=exp2(x,y+1)]

Join, 88, 165

167  y+1 e p

Detach, 94, 166

Case 2

As Required:

168  ~x=0 => y+1 e p

4 Conclusion, 148

169  [x=0 => y+1 e p] & [~x=0 => y+1 e p]

Join, 147, 168

170  y+1 e p

Cases, 51, 169

As Required:

171  ALL(b):[b e p => b+1 e p]

4 Conclusion, 77

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

Join, 76, 171

As Required:

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

Detach, 46, 172

Prove: ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

Suppose...

174  y e n

Premise

175  y e n => y e p

U Spec, 173

176  y e p

Detach, 175, 174

Apply definition of p

177  y e p <=> y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

U Spec, 35

178  [y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]]

& [y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p]

Iff-And, 177

179  y e p => y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Split, 178

180  y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)] => y e p

Split, 178

181  y e n & [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

Detach, 179, 176

182  y e n

Split, 181

183  ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

Split, 181

As Required:

184  ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

4 Conclusion, 174

As Required:

185  ALL(a):[a e n

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

4 Conclusion, 31

Prove: ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp1(a,b)=exp2(a,b)]]

Suppose...

186  x e n & y e n

Premise

187  x e n

Split, 186

188  y e n

Split, 186

189  x e n

=> ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

U Spec, 185

190  ALL(b):[b e n => [~[x=0 & b=0] => exp1(x,b)=exp2(x,b)]]

Detach, 189, 187

191  y e n => [~[x=0 & y=0] => exp1(x,y)=exp2(x,y)]

U Spec, 190

192  ~[x=0 & y=0] => exp1(x,y)=exp2(x,y)

Detach, 191, 188

As Required:

193  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp1(a,b)=exp2(a,b)]]

4 Conclusion, 186

As Required:

194  ALL(exp1):ALL(exp2):[ALL(a):ALL(b):[a e n & b e n => exp1(a,b) e n]

& ALL(a):[a e n => exp1(a,2)=a*a]

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

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

& ALL(a):[a e n => exp2(a,2)=a*a]

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

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

4 Conclusion, 9