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 divide z
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.