How to formalize

[Dodo]

I increasingly find demonstrations in number theory that rely on verbal arguments, rather than a more algebraic proof involving notation. (I hope this is just my fault.)

For example, consider this simple statement,
"If n divides a.b but does not divide a or b individually, then n is composite and can be expressed as n = r.s, where r|a and s|b."

In order to prove it, I have to proceed like this: a prime factor in n must appear in either a or b; were n prime, if would divide either a or b. Thus it is composite, and made of prime factors coming from either a or b." Sort of.

Is there a way of not having to talk? Some formalism for this? (I hope so.) Otherwise I'd find number theory a bit lacking. Opinions welcome.

[Focus]

"If n divides a.b but does not divide a or b individually, then n is composite and can be expressed as n = r.s, where r|a and s|b."
(n|a.b \wedge (\neg(n|a\vee n|b)))\rightarrow (n=r.s \wedge r|a \wedge r|b)

[Dodo]

That's cool. Now what about the proof. :)

"And"s and "or"s are easy, but I find difficulty formalizing ideas around factorization. Maybe some abstract algebra (or a lot of it) should be taught before the number theory courses.

But my question is, after you've learned groups, UFDs, etc etc, (which is not my case yet), can proofs like the above be expressed in a less ambiguous format?

[CRGreathouse]

Maybe you're looking for something like this?
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.9916

[Focus]

That's cool. Now what about the proof. :)


I was hoping you wouldn't ask. The proof is gonna be a bit longer...

a prime factor in n must appear in either a or b; were n prime, if would divide either a or b. Thus it is composite, and made of prime factors coming from either a or b.
((k|n \wedge k \neq r.s)\rightarrow (k|a \vee k|b))\wedge ((n=r.s \wedge n \neq r.s) \equiv \bot) \wedge (\neg(n|a \vee n|b) \rightarrow n=r.s)) \wedge (n|a.b \wedge \neg(n|a \vee n|b)) \rightarrow (n=r.s \wedge r|a \wedge r|b)

I'm sure I made a mistake somewhere :blushing:, can't really concentrate for long. But something like this has no words.

[Dodo]

Thanks for the effort :)
I did not follow your expression in detail, but I think I can grasp a point from it: you'd express the condition of being prime or composite, by the existence (or not) of a divisor. (The divisor should not be 1 or the number itself, though.)

It's still too cumbersome. Nobody would move an inch to communicate with another human being if s/he had to go through that. It's not that all words had to be eliminated; but I still miss some formalism to specifically speak about the list of prime factors of a number. Maybe I'm being too subjective, so maybe it's better to let the subject rest.

[CRGreathouse]

Metamath ( http://us.metamath.org/ ) may be along the lines you're thinking: a formalization of large chunks of mathematics. Mizar is similar, though I don't know as much about it.

[snipez90]

Well the thing I love about elementary number theory is that it lends itself to intuitive understanding. But I haven't seen many proofs that are entirely verbal and without notation. In a sense an elementary proof may not be "formal" in notation but if it appeals to intuition then it's fine by me.

"If n divides a.b but does not divide a or b individually, then n is composite and can be expressed as n = r.s, where r|a and s|b."

Suppose n is prime. Then by Euclid's lemma, n|ab \Rightarrow n|a or n|b . But we claimed that n does not divide a or b individually. Hence, n is composite.

Euclid's lemma can be proved but it is so intuitively clear. Similarly, the fact that n can be decomposed into two parts such that one divides a and the other divides b also appeals to intuition. Personally, I prefer starting out with problems and proofs like these before getting formal.