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)

Dan
Visit my new math blog at http://www.dcproof.wordpress.com

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

THEOREM 1

There 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 2

All "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 = 9

A 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 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/T3-Product-of-Powers.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/T4-Power-of-a-Power.htm (143 lines)

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

THEOREM 6 (Lemma): Non-Zero Powers

ALL(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 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/T6-Power-of-a-product.htm (199 lines)