Date: Oct 23, 2013 5:36 PM
Subject: Re: Formal proof of the ambiguity of 0^0
On 10/23/2013 11:55 AM, Dan Christensen wrote:
> As some have suggested here, context may have a bearing on this matter, but care should be taken so as not confuse the subtly different concepts.
> We could have two different functions: what might be called multiplicative exponentiation (x^y, the usual kind), and what might be called combinatorial exponentiation (f where f(x,y) = 1 if x=y=0, = x^y otherwise). Perhaps a different notation should be used for each where it matters, e.g. in formal, foundational proofs.
Let me thank you for reminding
me of that with these threads.
By the way, you should have taken
the challenge. Quasi found a fatal
error. It seems easily fixed, though.
The new sentence will be
AxAy( x mdiv y <-> ( Az( y pdiv z -> x mdiv z ) /\ Az( z pdiv x -> Aw( z
mdiv w ) ) ) )
Az( y pdiv z -> x mdiv z )
says that if y properly divides any z,
then 1 and all of its prime divisors also
Az( z pdiv x -> Aw( z mdiv w ) ) ) )
says that if any z can properly divide x
then it must be a monadic divisor for every
w. But, a monadic divisor is either 1 or
a prime. So, it has to be 1.
As for context here in contrast with other
contexts, Skolem introduced primitive recursive
arithmetic precisely because he wished to
avoid the use of quantifiers. Where the arithmetic
of 0 has no place in a construction like this, it
is extremely useful in the recursive definitions
often used in first-order Peano arithmetic.
My thanks is sincere. I had been wondering how I
might extend certain ideas of my own into an arithmetical
theory. Your threads motivated me for better or worse.