Oh, the ambiguity!

IntroductionMost of us learned in high school that 0

^{0}is somehow undefined or ambiguous. In college or university courses, your calculus instructors will confirm this, while your computer science instructors may tell you to conveniently set it equal to one – convenient for, among other things, applications of the Binomial Theorem. They say there would be too many exceptions to consider otherwise. The fence-sitters will say 0^{0}is undefined for continuous (real number) variables, but 0^{0}= 1 for the discrete variables (the natural numbers, here including zero).How can we formalize this ambiguous notion? Here, I will argue, using formal and informal methods that even in the case of discrete variables (using the natural numbers including 0), we should probably leave 0

^{0}undefined. This is nothing new or radical. It has more or less been the norm since Cauchy's famous list of indeterminate forms was first published nearly two centuries ago in 1821. If there is anything new here, it is just the rationale I present for leaving 0^{0}undefined, one based on a formal analysis including hundreds of lines of machine-verified formal proof.

Repeated Arithmetic OperationsEarly on our mathematical careers, we learned that multiplication (*) is just repeated addition, and exponentiation (^) is just repeated multiplication. We can informally define them as follows.

Multiplication (*) Defined as Repeated Addition:For any

ainN, we have:

a*2 =a+a

a*3 =a+a+a

a*4 =a+a+a+aand so on.

(We assume that addition and its basic algebraic properties, e.g. associativity, commutativity, cancelability, have already been well established.)

Exponentiation (^) Defined as Repeated Multiplication:For any

ainN, we have:

a^2 =a*a

a^3 =a*a*a

a^4 =a*a*a*aand so on.

What about a*1 and a*0?Since it takes at least two numbers to do addition, how we can assign values to

a*1 anda*0 using the above table? We can more reasonably ask, which functions of two variables on the natural numbers satisfy the above requirements for multiplication?To answer this question, we should note that the above requirements for repeated addition on

Ncan be summarized in just two formulas:1.

a*2 =a+a2.

a*(b+1) =a*b+aUsing these formulas, we can use the established properties of addition to prove that

a*1 =aanda*0 = 0 for allainN. (Left as an exercise for the reader. Hint: Consider the cases ofb=1 , thenb= 0 .)

Thus, we can fill in the entire multiplication table using

onlythe above definition of multiplication. And we have auniquefunction * onallof N that satisfies the above conditions.An equivalent and much more easier definition to work with would be:

1.

a*0 = 02.

a*(b+1) =a*b+a

What about a^1 and a^0?It turns out that, unlike the case with multiplication, there is not just one function that satisfies the above conditions for the ^ operator ─ there are

infinitelymany such functions. We can demonstrate this informally by filling a table of values.First, note that the above requirements for repeated multiplication on N can be summarized in two formulas:

2.

a^(b+1) =a^b*aWe start by filling in the third row for the exponent 2 using (1) .

Next, we can fill in the rows for all the exponents greater than 2 using (2).

Now, we fill in the powers of 2 in the third column.

Determine 2^1

^{Using (2), we have 2^2 = 2^(1+1) = 2^1 * 2 Using (1), we have 2^2 = 2 * 2 Substituting, 2^1 * 2 = 2 * 2 }

Cancelling, we obtain 2^1 = 2.

Determine 2^0Using (2), we have 2^1 = 2^(0+1) = 2^0 * 2

From previous result, we have 2^1 = 2 = 1*2

Substituting, we have 2^0 * 2 = 1 *2

Cancelling, we obtain 2^0 = 1

Similarly, we fill in the columns for all non-zero exponents.

Since we cannot cancel factors of zero, we need a different approach for the remaining powers of zero.

We let 0

^{0 }=x_{0}.

Determine 0^1Using (2), we have 0^1 = 0^(0+1) = 0^0 * 0 =

x_{0}* 0 = 0 whatever valuex_{0}may have.

The value of 0^0, whatever it might be, has no effect on the rest of the table. Any value for 0^0 will satisfy the above requirements for exponentiation. Therefore, infinitely many functions on N will satisfy the above requirements for exponentiation. Hence the ambiguity.

Theorem 1In DC Proof format:

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 => pow(a,2)=a*a]

& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]](Formal proof 1,107 lines)

Fortunately, they disagree

onlywhen the base and exponent are both zero. Otherwise, all functions that satisfy the requirements for exponentiation are in complete agreement.In DC Proof format:

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

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

& 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]

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

& 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)]](Formal proof 386 lines)

It should then be possible to construct a unique

partialfunction ^ on NxN, one that is defined for every point in NxN but (0, 0) . We could then define exponentiation as follows:1. 0^1 = 0

2.

a^2 =a*afor allainN3.

a^(b+1) =a^b*afor alla,binNand nota=b= 0An equivalent and much easier definition to work would with be:

1.

a^0 = 1 for all non-zeroainN2. 0^1 = 0

3.

a^(b+1) =a^b* a for alla,binNand nota=b= 0

In DC Proof format:

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

& pow(0,1)=0

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

& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

=> pow(a,b+1)=pow(a,b)*a]]EXIST(pow):[ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => pow(a,b) e n]

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

& pow(0,1)=0

& ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0]

=> pow(a,b+1)=pow(a,b)*a]]Formal proof 479 lines)

Why not 0^0 = 1?By various methods, the proponents of 0^0 = 1 have essentially constructed an exponentiation function ^ on

Nsuch that:1.

x^0 = 1 for allxinN2.

x^(y+1) =x^y*xIt doesn't really matter how it was constructed. What matters is whether or not the function so constructed

uniquelymeets the requirements of exponentiation as repeated multiplication as above.As we saw in Theorem 2, this is only one of infinitely many binary functions ^ on

allofNthat satisfies these requirements. We also saw in Theorem 3 that we can construct a partial function ^ onNxN(excluding only the point (0, 0) in the domain of definition) that doesuniquelymeet these requirements in this particular domain. As such, it is probably best to leave 0^0 undefined even in the case of discrete variables.

The Laws of ExponentsUsing the above definition, we can derive the Laws of Exponents just like they taught you in high school.

1. The Product of Powers Rule: a

^{b}. a^{c}= a^{b+c}for all non-zero a in NALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b*a^c=a^(b+c)]

(Formal proof 159 lines)

2. The Power of a Power Rule: (a

^{b})^{c}= a^{b}^{.c}for all non-zero a in NALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=0 => a^b^c=a^(b*c)]

(Formal proof 162 lines)

3. The Power of a Product Rule: (a.b)

^{c}= a^{c}. b^{c}for all non-zero a, b in NALL(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]

(Formal proof 200 lines)