Oh, the ambiguity!

Introduction

Most of us learned in high school that 00 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 00 is undefined for continuous (real number) variables, but 00 = 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 00 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 00 undefined, one based on a formal analysis including hundreds of lines of machine-verified formal proof.

Repeated Arithmetic Operations

Early 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 a in N, we have:

a*2 = a+a

a*3 = a+a+a

a*4 = a+a+a+a

and 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 a in N, we have:

a^2 = a*a

a^3 = a*a*a

a^4 = a*a*a*a

and so on.

Since it takes at least two numbers to do addition, how we can assign values to a*1 and a*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 N can be summarized in just two formulas:

1. a*2 = a + a

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

Using these formulas, we can use the established properties of addition to prove that a*1 = a and a*0 = 0 for all a in N. (Left as an exercise for the reader. Hint: Consider the cases of b =1 , then b = 0 .)

Thus, we can fill in the entire multiplication table using only the above definition of multiplication. And we have a unique function * on all of N that satisfies the above conditions.

An equivalent and much more easier definition to work with would be:

1. a*0 = 0

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

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 infinitely many 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:

1. a^2 = a * a

2. a^(b+1) = a^b * a

We 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^0

Using (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 00 = x0.

Determine 0^1

Using (2), we have 0^1 = 0^(0+1)   = 0^0 * 0 = x0 * 0  = 0 whatever value x0 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 1

In 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 only when the base and exponent are both zero. Otherwise, all functions that satisfy the requirements for exponentiation are in complete agreement.

Theorem 2

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 partial function ^ 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*for all a in N

3.  a^(b+1) = a^b * a for all a, b in N and not a = b = 0

An equivalent and much easier definition to work would with be:

1. a^0 = 1 for all non-zero a in N

2. 0^1 = 0

3. a^(b+1) = a^b * a for  all a, b in N and not a = b = 0

Theorem 3

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 N such that:

1.   x^0 = 1  for all x in N

2.  x^(y+1) = x^y * x

It doesn't really matter how it was constructed. What matters is whether or not the function so constructed uniquely meets 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 all of N  that satisfies these requirements. We also saw in Theorem 3 that we can construct a partial function ^ on NxN (excluding only the point (0, 0) in the domain of definition) that does uniquely meet 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 Exponents

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

1.  The Product of Powers Rule:  ab . ac = ab+c  for all non-zero a in

ALL(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:  (ab)c = ab.c  for all non-zero a in N

ALL(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 = ac . bc  for all non-zero a, b in N

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]

200 lines)

Follow-up, 2019-02-12

Theorem

ALL(x1):ALL(x2):[x1 e n & x2 e n

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

& exp(0,0)=x1

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

& ALL(a):ALL(b):[a e n & b e n => exp(a,b+1)=exp(a,b)*a]

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

& exp'(0,0)=x2

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

& ALL(a):ALL(b):[a e n & b e n => exp'(a,b+1)=exp'(a,b)*a]

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

(Formal proof 66 lines)