Informal Introduction
*********************
Here, we formally justify leaving 0^0 undefined on the set of natural numbers n. We assume that the Product of Powers Rule holds on n.
(This proof was written with the aid of the author's DC Proof software available at
Basic arithmetic required
*************************
+ is a binary function on n
1 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
* is a binary function on n
2 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
3 0 e n
Axiom
4 1 e n
Axiom
5 2 e n
Axiom
6 2=1+1
Axiom
0 is additive identity element
7 ALL(a):[a e n => a+0=a]
Axiom
Zero products
8 ALL(a):[a e n => a*0=0]
Axiom
1 is the multiplicative identity element
9 ALL(a):[a e n => a*1=a]
Axiom
Commutativity of +
10 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Commutativity of *
11 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right cancelability of *
12 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~b=0 => [a*b=c*b => a=c]]]
Axiom
Zero products
13 ALL(a):[a e n => [a*a=0 => a=0]]
Axiom
Identity products
14 ALL(a):[a e n => [a*a=a => a=0 | a=1]]
Axiom
Definition of ^
***************
15 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Axiom
16 ALL(a):[a e n => a^2=a*a]
Axiom
17 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Axiom
Prove: ALL(a):[a e n => [~a=0 => a=a^1]]
Suppose...
18 x e n
Premise
Prove: ~x=0 => x=x^1
Suppose...
19 ~x=0
Premise
Apply defintion of ^
20 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
21 x e n & 1 e n => x^(1+1)=x^1*x
U Spec, 20
22 x e n & 1 e n
Join, 18, 4
23 x^(1+1)=x^1*x
Detach, 21, 22
24 x^2=x^1*x
Substitute, 6, 23
Apply definiton of ^
25 x e n => x^2=x*x
U Spec, 16
26 x^2=x*x
Detach, 25, 18
27 x*x=x^1*x
Substitute, 26, 24
Apply right cancelability of *
28 ALL(b):ALL(c):[x e n & b e n & c e n => [~b=0 => [x*b=c*b => x=c]]]
U Spec, 12
29 ALL(c):[x e n & x e n & c e n => [~x=0 => [x*x=c*x => x=c]]]
U Spec, 28
30 x e n & x e n & x^1 e n => [~x=0 => [x*x=x^1*x => x=x^1]]
U Spec, 29
31 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
32 x e n & 1 e n => x^1 e n
U Spec, 31
33 x e n & 1 e n
Join, 18, 4
34 x^1 e n
Detach, 32, 33
35 x e n & x e n
Join, 18, 18
36 x e n & x e n & x^1 e n
Join, 35, 34
37 ~x=0 => [x*x=x^1*x => x=x^1]
Detach, 30, 36
38 x*x=x^1*x => x=x^1
Detach, 37, 19
39 x=x^1
Detach, 38, 27
As Required:
40 ~x=0 => x=x^1
4 Conclusion, 19
As Required:
41 ALL(a):[a e n => [~a=0 => a=a^1]]
4 Conclusion, 18
As Required:
42 ALL(a):[a e n => [~a=0 => a^1=a]]
Sym, 41
Prove: ALL(a):[a e n => [~a=0 => a^0=1]]
Suppose...
43 x e n
Premise
Prove: ~x=0 => x^0=1
Suppose...
44 ~x=0
Premise
Apply definition of ^
45 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 17
46 x e n & 0 e n => x^(0+1)=x^0*x
U Spec, 45
47 x e n & 0 e n
Join, 43, 3
48 x^(0+1)=x^0*x
Detach, 46, 47
49 1 e n => 1+0=1
U Spec, 7
50 1+0=1
Detach, 49, 4
Prove: 0+1=1
51 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 10
52 1 e n & 0 e n => 1+0=0+1
U Spec, 51
53 1 e n & 0 e n
Join, 4, 3
54 1+0=0+1
Detach, 52, 53
55 0+1=1
Substitute, 54, 50
56 x^1=x^0*x
Substitute, 55, 48
57 x e n => [~x=0 => x=x^1]
U Spec, 41
58 ~x=0 => x=x^1
Detach, 57, 43
59 x=x^1
Detach, 58, 44
60 x=x^0*x
Substitute, 59, 56
61 x e n => x*1=x
U Spec, 9
62 x*1=x
Detach, 61, 43
63 x*1=x^0*x
Substitute, 62, 60
Apply previous result
64 ALL(b):[x e n & b e n => x*b=b*x]
U Spec, 11
65 x e n & 1 e n => x*1=1*x
U Spec, 64
66 x e n & 1 e n
Join, 43, 4
67 x*1=1*x
Detach, 65, 66
68 1*x=x^0*x
Substitute, 67, 63
Apply right cancealability of *
69 ALL(b):ALL(c):[1 e n & b e n & c e n => [~b=0 => [1*b=c*b => 1=c]]]
U Spec, 12
70 ALL(c):[1 e n & x e n & c e n => [~x=0 => [1*x=c*x => 1=c]]]
U Spec, 69
71 1 e n & x e n & x^0 e n => [~x=0 => [1*x=x^0*x => 1=x^0]]
U Spec, 70
72 ALL(b):[x e n & b e n => x^b e n]
U Spec, 15
73 x e n & 0 e n => x^0 e n
U Spec, 72
74 x e n & 0 e n
Join, 43, 3
75 x^0 e n
Detach, 73, 74
76 1 e n & x e n
Join, 4, 43
77 1 e n & x e n & x^0 e n
Join, 76, 75
78 ~x=0 => [1*x=x^0*x => 1=x^0]
Detach, 71, 77
79 1*x=x^0*x => 1=x^0
Detach, 78, 44
80 1=x^0
Detach, 79, 68
81 x^0=1
Sym, 80
As Required:
82 ~x=0 => x^0=1
4 Conclusion, 44
As Required:
83 ALL(a):[a e n => [~a=0 => a^0=1]]
4 Conclusion, 43
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^(b+c)=a^b*a^c]
=> 0^1=0 & [0^0=0 | 0^0=1]
Suppose the Product of Powers Rule (PPR) holds for exponentiation on N
84 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^(b+c)=a^b*a^c]
Premise
Apply PPR
85 ALL(b):ALL(c):[0 e n & b e n & c e n => 0^(b+c)=0^b*0^c]
U Spec, 84
86 ALL(c):[0 e n & 1 e n & c e n => 0^(1+c)=0^1*0^c]
U Spec, 85
87 0 e n & 1 e n & 1 e n => 0^(1+1)=0^1*0^1
U Spec, 86
88 0 e n & 1 e n
Join, 3, 4
89 0 e n & 1 e n & 1 e n
Join, 88, 4
90 0^(1+1)=0^1*0^1
Detach, 87, 89
91 0^2=0^1*0^1
Substitute, 6, 90
92 0 e n => 0^2=0*0
U Spec, 16
93 0^2=0*0
Detach, 92, 3
94 0*0=0^1*0^1
Substitute, 93, 91
95 0 e n => 0*0=0
U Spec, 8
96 0*0=0
Detach, 95, 3
97 0=0^1*0^1
Substitute, 96, 94
98 0^1 e n => [0^1*0^1=0 => 0^1=0]
U Spec, 13
Apply definition of ^
99 ALL(b):[0 e n & b e n => 0^b e n]
U Spec, 15
100 0 e n & 1 e n => 0^1 e n
U Spec, 99
101 0 e n & 1 e n
Join, 3, 4
102 0^1 e n
Detach, 100, 101
103 0^1*0^1=0 => 0^1=0
Detach, 98, 102
104 0^1*0^1=0
Sym, 97
As Required:
105 0^1=0
Detach, 103, 104
Apply PPR
106 ALL(b):ALL(c):[0 e n & b e n & c e n => 0^(b+c)=0^b*0^c]
U Spec, 84
107 ALL(c):[0 e n & 0 e n & c e n => 0^(0+c)=0^0*0^c]
U Spec, 106
108 0 e n & 0 e n & 0 e n => 0^(0+0)=0^0*0^0
U Spec, 107
109 0 e n & 0 e n
Join, 3, 3
110 0 e n & 0 e n & 0 e n
Join, 109, 3
111 0^(0+0)=0^0*0^0
Detach, 108, 110
112 0 e n => 0+0=0
U Spec, 7
113 0+0=0
Detach, 112, 3
114 0^0=0^0*0^0
Substitute, 113, 111
115 0^0 e n => [0^0*0^0=0^0 => 0^0=0 | 0^0=1]
U Spec, 14
116 ALL(b):[0 e n & b e n => 0^b e n]
U Spec, 15
117 0 e n & 0 e n => 0^0 e n
U Spec, 116
118 0 e n & 0 e n
Join, 3, 3
119 0^0 e n
Detach, 117, 118
120 0^0*0^0=0^0 => 0^0=0 | 0^0=1
Detach, 115, 119
121 0^0*0^0=0^0
Sym, 114
As Required:
122 0^0=0 | 0^0=1
Detach, 120, 121
123 0^1=0 & [0^0=0 | 0^0=1]
Join, 105, 122
As Required:
124 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^(b+c)=a^b*a^c]
=> 0^1=0 & [0^0=0 | 0^0=1]
4 Conclusion, 84
125 ALL(a):[a e n => [~a=0 => a^1=a]]
& ALL(a):[a e n => [~a=0 => a^0=1]]
Join, 42, 83
As Required:
126 ALL(a):[a e n => [~a=0 => a^1=a]]
& ALL(a):[a e n => [~a=0 => a^0=1]]
& [ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a^(b+c)=a^b*a^c]
=> 0^1=0 & [0^0=0 | 0^0=1]]
Join, 125, 124