
Formal proof of the ambiguity of 0^0
Posted:
Oct 16, 2013 11:21 PM


To followup 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)
Dan Download my DC Proof 2.0 software at http://www.dcproof.com Visit my new math blog at http://www.dcproof.wordpress.com
************************
THEOREM 1
There exists infinitely many "exponentlike" 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/T1Constructpowfunction.htm (1,038 lines)
************************
THEOREM 2
All "exponentlike" 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 exponentlike functions such that pow(0,0)=x0 and pow'(0,0)=x1.
http://dcproof.com/Powfunctionsidentical.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 "exponentlike" 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 = 9
A little exercise in using the above definition.
http://dcproof.com/T23cubed.htm (61 lines)
************************
Note: The remaining proofs derive the usual Laws of Exponents from the above definition.
************************
THEOREM 4: The Product of Powers Rule
ALL(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/T3ProductofPowers.htm (147 lines)
************************
THEOREM 5: The Power of a Power Rule
ALL(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/T4PowerofaPower.htm (143 lines)
************************
THEOREM 6 (Lemma): NonZero Powers
ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
http://dcproof.com/T5Nonzeropowers.htm (105 lines)
************************
THEOREM 7: The Power of a Product Rule
ALL(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/T6Powerofaproduct.htm (199 lines)

