[FOM] Perfect Powers

[A. Mani]

Vaughan Pratt <pratt at cs.stanford.edu>
> What does it mean for a proof to be "algebraic?"

A proof that avoids predicates that are not representable and is 'quasi-
equational'. In this problem, it is ok to quantify over Q or Z.  
 
Of course 'quasi-equational' part can be relaxed substantially, but here it 
does not seem to be essential.  

> Since the prime factorization theorem can be proved in a couple of 
> lines, I'm not sure what to make of your "much simpler."  

It assumes the division algorithm and needs the concept of prime numbers 
(while 'relatively prime' is sufficient).

> But from your 
> mention of floor I imagine you must have essentially the following proof 
> in mind.
> 
> Given p^{1/q} = m/n with (m,n) = 1, n > 0, we want to show n = 1.  So 
> suppose to the contrary that n >= 2.  Then p = (m/n)^q, so pn^q = m^q. 
> Hence m^q mod n = 0.  But since m is in the reduced residue system mod 
> n, so is m^q whence it cannot be zero there.  QED.

In that form, the proof does not fit as the equivalence requires existential 
quantifiers.      

I was thinking of the following constructive proof:

Let p^{1/q} = m/n with (m,n) = 1, n > 0;    

and c= n(p^{1/q} - f(p^{1/q}))  (f being the floor fn)

Since 0 \leq (p^{1/q} - f(p^{1/q})) < 1

0 \leq c < n

But c (m/n)^{q-1} = c(p^{1/q})^{q-1} = 
= n(p^{1/q})^{q} - nf(p^{1/q}) (m/n)^{q-1} 

Multiplying both sides of the eqn by n^{q-2}, we get

(c m^{q-1}) /n  = (n^{q-1})p - f(p^{1/q}) m^{q-1} (an integer)

So, n | cm^{q-1} => n|c

But c \in [0,n) => c = 0

(this proof can be adapted to the better systems in craig's 1989-90 paper(s) 
in JSL)


Best

A. Mani

 

-- 
A. Mani
ASL, CLC, AMS, CMS
http://www.logicamani.co.cc