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 Language Example - Human-Readable?
Replies: 39   Last Post: Jun 27, 2009 11:09 PM

 Messages: [ Previous | Next ]
 Andrew Tomazos Posts: 137 Registered: 8/1/05
Re: Formal Proof Language Example - Human-Readable?
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) * (c-a)
> >> n*q*m*n*q*m = n*q*n * q*m*m    (factorization of b, c+a, c-a sic!)

>
> > In this step you have used:
>
> >   b = n*q*m
> >   c+a = q*n*n
> >   c-a = 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)*(c-a)=n*q*m*n*q*m follows also, since factors are unique,
> the same classes also occure in the product (c+a)*(c-a).
>
> 1) Now if a factor does not occur in (c+a) then it occurs twice in
> (c-a), this is the class m.
>
> 2) Further if a factor does not occur in (c-a) 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 (c-a)),
> then it occurs in (c+a) and it occurs in (c-a), 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.

Date Subject Author
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Andrew Tomazos
6/21/09 Jan Burse
6/21/09 Jan Burse
6/24/09 Andrew Tomazos
6/25/09 MeAmI.org
6/25/09 Jan Burse
6/26/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Jan Burse
6/27/09 Andrew Tomazos
6/27/09 Joshua Cranmer
6/27/09 Andrew Tomazos
6/21/09 Marshall
6/21/09 Spiros Bousbouras
6/24/09 Tim Smith
6/21/09 Charlie-Boo
6/21/09 William Elliot
6/22/09 MeAmI.org
6/22/09 MeAmI.org
6/23/09 Slawomir
6/24/09 David Bernier
6/24/09 MeAmI.org
6/24/09 MeAmI.org
6/24/09 Andrew Tomazos
6/24/09 Andrew Tomazos
6/25/09 Slawomir