Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: Formal proof of the ambiguity of 0^0
Replies: 163   Last Post: Nov 13, 2013 10:45 AM

 Messages: [ Previous | Next ]
 Dan Christensen Posts: 8,219 Registered: 7/9/08
Formal proof of the ambiguity of 0^0
Posted: Oct 16, 2013 11:21 PM

To follow-up on my previous postings at sci.math on this topic, here are links to 7 formal proofs (in the DC Proof 2.0 format) supporting the notion that 0^0 be left undefined. (Notation: 'e' = epsilon, set membership, n = the set of natural numbers including 0)

Dan
Visit my new math blog at http://www.dcproof.wordpress.com

************************

THEOREM 1

There exists infinitely many "exponent-like" functions ? one for each natural number x0.

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 => [~a=0 => pow(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]]

http://dcproof.com/T1-Construct-pow-function.htm (1,038 lines)

************************

THEOREM 2

All "exponent-like" functions are identical except for the value assigned to (0,0).

ALL(pow):ALL(x0):ALL(pow'):ALL(x1):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
& 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]
& pow'(0,0)=x1
& ALL(a):[a e n => [~a=0 => pow'(a,0)=1]]
& 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)]]]

where pow and pow' are exponent-like functions such that pow(0,0)=x0 and pow'(0,0)=x1.

http://dcproof.com/Pow-functions-identical.htm (266 lines)

************************

Note: In subsequent theorems here, we will define the exponent operator '^' as follows:

ALL(a):ALL(b):[a e n & b e n => a^b e n]
& ALL(a):[a e n => [~a=0 => a^0=1]]
& ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]

From Theorem 1, we know that functions satisfying these conditions do exist. These are characteristics of all "exponent-like" functions. Here, 0^0 is assumed to be a natural number, but it is not assumed to have any particular value.

************************

THEOREM 3: 3^2 = 9

A little exercise in using the above definition.

http://dcproof.com/T2-3-cubed.htm (61 lines)

************************

Note: The remaining proofs derive the usual Laws of Exponents from the above definition.

************************

THEOREM 4: The Product of Powers Rule

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [~a=0 => a^b*a^c=a^(b+c)]]

http://dcproof.com/T3-Product-of-Powers.htm (147 lines)

************************

THEOREM 5: The Power of a Power Rule

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [~a=0 => (a^b)^c=a^(b*c)]]

http://dcproof.com/T4-Power-of-a-Power.htm (143 lines)

************************

THEOREM 6 (Lemma): Non-Zero Powers

ALL(a):ALL(b):[a e n & b e n
=> [~a=0 => ~a^b=0]]

http://dcproof.com/T5-Non-zero-powers.htm (105 lines)

************************

THEOREM 7: The Power of a Product Rule

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]]

http://dcproof.com/T6-Power-of-a-product.htm (199 lines)

Date Subject Author
10/16/13 Dan Christensen
10/16/13 Brian Q. Hutchings
11/1/13 ross.finlayson@gmail.com
10/17/13 Robin Chapman
10/17/13 Bart Goddard
10/17/13 Dan Christensen
10/17/13 fom
10/17/13 Bart Goddard
10/17/13 Dan Christensen
10/17/13 Bart Goddard
10/17/13 Dan Christensen
10/17/13 Peter Percival
10/17/13 Dan Christensen
10/17/13 Dan Christensen
11/2/13 Brian Q. Hutchings
10/17/13 Bart Goddard
10/17/13 Dan Christensen
10/18/13 Bart Goddard
10/17/13 Dan Christensen
10/17/13 Ben Bacarisse
10/17/13 Dan Christensen
10/17/13 Robin Chapman
10/17/13 Dan Christensen
10/17/13 Bart Goddard
10/17/13 Dan Christensen
10/17/13 Brian Q. Hutchings
10/17/13 Brian Q. Hutchings
10/18/13 Robin Chapman
10/18/13 Dan Christensen
10/23/13 Shmuel (Seymour J.) Metz
10/25/13 Bart Goddard
10/29/13 Dan Christensen
10/30/13 Bart Goddard
10/30/13 Dan Christensen
10/30/13 Bart Goddard
10/30/13 Dan Christensen
10/30/13 Bart Goddard
10/30/13 Robin Chapman
10/30/13 Bart Goddard
10/30/13 Peter Percival
10/30/13 Richard Tobin
10/30/13 fom
10/31/13 David Bernier
10/31/13 David Bernier
10/30/13 Dan Christensen
10/30/13 Bart Goddard
10/30/13 Dan Christensen
10/31/13 Bart Goddard
10/31/13 Dan Christensen
10/31/13 Bart Goddard
10/31/13 Dan Christensen
10/31/13 Bart Goddard
10/30/13 Peter Percival
10/30/13 JT
10/30/13 Dan Christensen
10/30/13 Peter Percival
10/30/13 Dan Christensen
10/30/13 Brian Q. Hutchings
10/30/13 Brian Q. Hutchings
10/30/13 JT
10/30/13 Peter Percival
10/30/13 JT
10/30/13 JT
10/30/13 Brian Q. Hutchings
10/18/13 Robin Chapman
10/18/13 Dan Christensen
10/18/13 fom
10/18/13 Dan Christensen
10/18/13 fom
10/18/13 Dan Christensen
10/18/13 Peter Percival
10/18/13 Dan Christensen
10/20/13 Dan Christensen
10/20/13 Bart Goddard
10/20/13 Dan Christensen
10/20/13 Bart Goddard
10/20/13 Dan Christensen
10/20/13 Bart Goddard
10/20/13 Michael F. Stemper
10/20/13 Bart Goddard
10/20/13 Dan Christensen
10/23/13 Brian Q. Hutchings
10/20/13 Dan Christensen
10/20/13 Bart Goddard
10/20/13 Dan Christensen
10/20/13 Bart Goddard
10/20/13 Dan Christensen
10/21/13 Bart Goddard
10/21/13 Dan Christensen
10/21/13 Peter Percival
10/21/13 Bart Goddard
10/21/13 Dan Christensen
10/21/13 Bart Goddard
10/21/13 Peter Percival
10/21/13 fom
10/21/13 Bart Goddard
10/21/13 JT
10/21/13 Dan Christensen
10/21/13 JT
10/21/13 Dan Christensen
10/20/13 Peter Percival
10/20/13 Dan Christensen
10/23/13 Dan Christensen
10/23/13 fom
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Dan Christensen
11/1/13 fom
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 Brian Q. Hutchings
11/1/13 Dan Christensen
11/1/13 Brian Q. Hutchings
11/2/13 Robin Chapman
11/1/13 Dan Christensen
11/1/13 Bart Goddard
11/1/13 ross.finlayson@gmail.com
11/3/13 ross.finlayson@gmail.com
11/3/13 Brian Q. Hutchings
11/1/13 Dan Christensen
11/2/13 Bart Goddard
11/2/13 Dan Christensen
11/2/13 Bart Goddard
11/12/13 Bart Goddard
11/12/13 Bart Goddard
11/12/13 Bart Goddard
11/12/13 Bart Goddard
11/13/13 Bart Goddard
11/13/13 Bart Goddard
11/2/13 Virgil
11/2/13 Dan Christensen
11/2/13 Bart Goddard
11/2/13 Paul
11/3/13 Bart Goddard
11/2/13 Dan Christensen
11/2/13 Dan Christensen
11/2/13 Ki Song
11/2/13 Virgil
11/2/13 Michael F. Stemper
11/2/13 Virgil
11/3/13 Michael F. Stemper
11/3/13 Robin Chapman
11/3/13 fom
11/3/13 Jussi Piitulainen
11/3/13 fom
11/4/13 Jussi Piitulainen
11/3/13 JT
11/3/13 JT
11/12/13 Dan Christensen
11/13/13 Dan Christensen