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 ]
 Robin Chapman Posts: 412 Registered: 5/29/08
Re: Formal proof of the ambiguity of 0^0
Posted: Oct 17, 2013 1:32 PM

On 17/10/2013 04:21, Dan Christensen wrote:

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

I like

EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& ALL(a):[a e n => pow(a,0)=1]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]

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

I like

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

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

I like

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

>
> THEOREM 3: 3^2 = 9

My favourite square!

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

I like

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> a^b*a^c=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)]]

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

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

That's nice.

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

I like

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

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