*Oh, the
ambiguity! *

**Introduction**

Most 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 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+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 *a*
in *N*, 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 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*

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 *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:

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 0^{0 }= *x*_{0}.

**Determine 0^1**

Using (2), we have 0^1 = 0^(0+1)
= 0^0 * 0 = *x*_{0} * 0 = 0 whatever value *x*_{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 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.

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 *N*x*N*,
one that is defined for every point in *N*x*N*
but (0, 0) . We could then define exponentiation as
follows:

1. 0^1 = 0

2. * a*^2 = *a***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

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 *N*x*N*
(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: * a ^{b}
.*

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: * (**a ^{b})^{c}*
=

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}*
=

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]

(Formal proof 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)