
Re: Formal Proof Language Example  HumanReadable?
Posted:
Jun 26, 2009 10:07 PM


On Jun 26, 12:30 am, Jan Burse <janbu...@fastmail.fm> wrote: > Andrew Tomazos schrieb: > > > On Jun 22, 4:01 am, Jan Burse <janbu...@fastmail.fm> wrote: > >> b*b = (c+a) * (ca) > >> n*q*m*n*q*m = n*q*n * q*m*m (factorization of b, c+a, ca sic!) > > > In this step you have used: > > > b = n*q*m > > c+a = q*n*n > > ca = q*m*m > > > How do you know that there exists n, q and m such that these three > > equalities hold? > > Andrew. > > By some pingeonhole principle. > > n, q and m are classes of factors of b. If a class c is empty > then c=1. If a class c contains factors j, k, etc.. then c=j*k*... > So the n, q and m are not itself necessary prime, they group > certain prime number factors. > > Each factor of b occurs twice in b*b, so b*b=n*q*m*n*q*m is trivial. > > And thus (c+a)*(ca)=n*q*m*n*q*m follows also, since factors are unique, > the same classes also occure in the product (c+a)*(ca). > > 1) Now if a factor does not occur in (c+a) then it occurs twice in > (ca), this is the class m. > > 2) Further if a factor does not occur in (ca) then it occurs twice in > (c+a), this is the class n. > > 3) If a factor does not (not occur in (c+a) and not occur in (ca)), > then it occurs in (c+a) and it occurs in (ca), this is the class q.
We can assume that theorems about the nature of integer factorization have previously been established  but which ones specifically would we use to prove your above statements?
I think it would be beneficial if we could compute q, n and m directly.
Perhaps we can define a divisble_by function. So for example:
(12 divisable_by 4) == true (12 divisable_by 5) == false
Then we could use facts about that function such as:
forall x, k in N given: x divisble_by k implies: thereexists y in N x = y*k
forall x, y, k in N given: x divisible_by k implies: (x*y) divisible_by k
forall x, y, z, k in N given: z = x*y z divisble_by k implies: (x divisble_by k) or (y divisble_by k)
What do you think? Which of these kind of theorems should we use as a basis? Andrew.

