In article <firstname.lastname@example.org>, Peter Percival <email@example.com> wrote:
> Dan Christensen wrote: > > > > > More formally, exponentiation can be defined as a binary function on > > the set of natural number N such that: > > Can be but isn't, except by you. Everyone else, when defining a > function on N, will start where N starts, viz at 0. > > > > > (1) Ax in N: x^2=x*x > > > > (2) Ax,y in N: x^(y+1) = x^y * x > > > > It can then be shown that: > > > > (1) Ax in N:(x=/=0 => x^1=x) > > > > (2) Ax in N:(x=/=0 => x^0=1) > > > > (3) Ax,y,z in N:(x^(y+z) = x^y * x^z) => 0^1=0 /\ (0^0=0 \/ 0^0=1) > > > > (Formal proof to follow.) > > > > Thus, if the Product of Powers Rule is to hold on N, 0^0 will be > > ambiguous -- being either 0 or 1. Unless one of these alternatives > > can be formally proven > > 0^0 = 1 _can_ be formally proven, if you use the right definition. > > If your definition of ^ doesn't tell you what 0^0 is (remember, we're > talking about the naturals here) then the definition is incomplete. > > If you want to define ^ on the positive integers only and then claim > that 0^0 isn't thereby defined, then you'd be right. But it is _you_ > who claim to be talking about N. > > > or shown to give rise to a contradiction, the > > prudent course is to leave 0^0 undefined.
There is a commonly used definition of the naturals in which 0 does not appear, so for those naturals definitions of 0^x or x^0 are irrelevant. --