> > 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.
-- Sorrow in all lands, and grievous omens. Great anger in the dragon of the hills, And silent now the earth's green oracles That will not speak again of innocence. David Sutton -- Geomancies