```Date: Oct 16, 2013 11:21 PM
Author: Dan Christensen
Subject: Formal proof of the ambiguity of 0^0

To follow-up on my previous postings at sci.math on this topic, here are links to 7 formal proofs (in the DC Proof 2.0 format) supporting the notion that 0^0 be left undefined. (Notation: 'e' = epsilon, set membership, n = the set of natural numbers including 0)DanDownload my DC Proof 2.0 software at http://www.dcproof.comVisit my new math blog at http://www.dcproof.wordpress.com************************THEOREM 1There exists infinitely many "exponent-like" functions  ? one for each natural number x0.ALL(x0):[x0 e n=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]& pow(0,0)=x0& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]]http://dcproof.com/T1-Construct-pow-function.htm (1,038 lines)************************THEOREM 2All "exponent-like" functions are identical except for the value assigned to (0,0). ALL(pow):ALL(x0):ALL(pow'):ALL(x1):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]& pow(0,0)=x0& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]& ALL(a):ALL(b):[a e n & b e n => pow'(a,b) e n]& pow'(0,0)=x1& ALL(a):[a e n => [~a=0 => pow'(a,0)=1]]& ALL(a):ALL(b):[a e n & b e n => pow'(a,b+1)=pow'(a,b)*a]=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => pow(a,b)=pow'(a,b)]]]where pow and pow' are exponent-like functions such that pow(0,0)=x0 and pow'(0,0)=x1.http://dcproof.com/Pow-functions-identical.htm (266 lines)************************Note: In subsequent theorems here, we will define the exponent operator '^' as follows:ALL(a):ALL(b):[a e n & b e n => a^b e n]& ALL(a):[a e n => [~a=0 => a^0=1]]& ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]From Theorem 1, we know that functions satisfying these conditions do exist. These are characteristics of all "exponent-like" functions. Here, 0^0 is assumed to be a natural number, but it is not assumed to have any particular value. ************************THEOREM 3: 3^2 = 9A little exercise in using the above definition. http://dcproof.com/T2-3-cubed.htm (61 lines)************************Note: The remaining proofs derive the usual Laws of Exponents from the above definition.************************THEOREM 4: The Product of Powers RuleALL(a):ALL(b):ALL(c):[a e n & b e n & c e n=> [~a=0 => a^b*a^c=a^(b+c)]]http://dcproof.com/T3-Product-of-Powers.htm (147 lines)************************THEOREM 5: The Power of a Power RuleALL(a):ALL(b):ALL(c):[a e n & b e n & c e n=> [~a=0 => (a^b)^c=a^(b*c)]]http://dcproof.com/T4-Power-of-a-Power.htm (143 lines)************************THEOREM 6 (Lemma):  Non-Zero PowersALL(a):ALL(b):[a e n & b e n=> [~a=0 => ~a^b=0]]http://dcproof.com/T5-Non-zero-powers.htm (105 lines)************************THEOREM 7:  The Power of a Product RuleALL(a):ALL(b):ALL(c):[a e n & b e n & c e n=> [~a=0 & ~b=0 => (a*b)^c=a^c*b^c]]http://dcproof.com/T6-Power-of-a-product.htm (199 lines)
```