Date: Nov 1, 2013 9:38 AM
Author: Dan Christensen
Subject: Re: Formal proof of the ambiguity of 0^0
On Friday, November 1, 2013 6:05:18 AM UTC-4, Bart Goddard wrote:
> Dan Christensen <Dan_Christensen@sympatico.ca> wrote in
> > Here, I prove 0^x = 0 for x=/=0
> The proof is fatally flawed. If y = 1, then z = 0,
> in which case the "proof" is threaded with the
> "uspecified" phrase "0^0."
On the contrary, this is not a problem at all. Again, 0^0 is a natural number, but no value is assigned to it in my definition of ^ on N. This formalizes the longstanding practice (since Cauchy in the early 19th century) of leaving 0^0 undefined. Again, I define ^ as follows:
1. ALL(a):ALL(b):[a e n & b e n => a^b e n] (i.e. ^ is a binary function on N)
2. ALL(a):[a e n => [~a=0 => a^0=1]]
3. ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
These 3 statements characterize ALL exponent-like functions on N (Theorem 1). And ALL exponent-like functions on N are identical except for the value assigned to (0,0). (Theorem 2).
No value is assigned to 0^0, but as readers can see for themselves from the theorems posting here, it is really quite easy to work around this minor inconvenience.
Download my DC Proof 2.0 software at http://www.dcproof.com
Visit my new math blog at http://www.dcproof.wordpress.com