What's the difference b/w a formal and an informal proof, in mathematics? I have an informal proof that sqrt(2) is irrational:
1. Assume sqrt(2)=x/y, where x and y are nonzero integers and relatively prime 2. y*sqrt(2)=x 3. 2y^2=x^2 4. x=2z, since x^2 is even by this, since it is able to be divided by 2, and it and the lhs are equal 5. 2y^2=(2z)^2=4z^2 6. y^2=2z^2 7. According line 4, since x is even, y must also be even 8. But then they must both share a factor, 2. But this contradicts our assumption that x and y do not share a common factor 9. Therefore, sqrt(2) is irrational
Btw, is there a less messy version of this?
This is an informal proof, but what's the formal proof?
> What's the difference b/w a formal and an informal proof, in > mathematics?
Basically, a formal proofs presents ALL the details left out in an informal proof; moreover it is ruled by a strict syntax; i.e. it's form is regimented by strict syntactical rules, etc. etc.
In short: completely formal proof are extremely tedious, and in practice impractical. Though they exhibit complete formal rigor.
"For every line of Cantor's list it is true that this line does not contain the diagonal number. Nevertheless the diagonal number may be in the infinite list." (WM, sci.logic)
On Jul 24, 1:38 pm, Protoman <Protoman2...@gmail.com> wrote:
> What's the difference b/w a formal and an informal proof, in > mathematics?
Style only. Importantly, this means no difference in rigor. A typical informal proof in mathematics is every bit as rigorous as a formal proof. The tacit guarantee is that from any informal proof a formal version can always be constructed, if challenged to do so.
> What's the difference b/w a formal and an informal proof, in > mathematics? I have an informal proof that sqrt(2) is irrational:
> 1. Assume sqrt(2)=x/y, where x and y are nonzero integers and > relatively prime > 2. y*sqrt(2)=x > 3. 2y^2=x^2 > 4. x=2z, since x^2 is even by this, since it is able to be divided by > 2, and it and the lhs are equal > 5. 2y^2=(2z)^2=4z^2 > 6. y^2=2z^2 > 7. According line 4, since x is even, y must also be even > 8. But then they must both share a factor, 2. But this contradicts our > assumption that x and y do not share a common factor > 9. Therefore, sqrt(2) is irrational
> Btw, is there a less messy version of this?
> This is an informal proof, but what's the formal proof?
> Thanks!
It is my belief that "formal proof" has no fixed meaning. What it might mean in this case is:
(i) choose a formulation of first order Peano Arithmetic (that requires that you first choose a formulation of first order logic) call it "PA",
(ii) express "sqrt 2 is irrational" in PA, call that expression "phi",
(iii) prove that PA |- phi.
For (iii), note that when (and only when) the details of the Peano Arithmetic have been fixed "prove that PA |- ..." has a precise meaning.
If "formal proof" were to have a fixed meaning then the impossible would need to happen: the ICU (say) would have to lay down the law that nothing is a formal proof unless it is expressed in such-and-such a set theory.
It seems to me that the point of formal proofs is not that they prove something, but rather that they are mathematical objects that are themselves amenable to mathematical study, say in the style of Hilbert's proof theory.
Btw, I would replace your steps 4 and 7 by applications of a lemma:
If p^2 is even then p is even.
As for "informal proof", I thinks it's a sociological and psychological thing: an informal proof is a presentation (written or spoken) by person X to person Y that results in Y believing something that X claims to be so. Note that the believing does not have to occur on first reading or hearing the proof: Y may have to spend time filling in details. Different Y's will feel the need to fill in more or less amounts of detail. Sometimes one says that X _and_ Y proved the claim, see FLT.
-- He is not here; but far away The noise of life begins again And ghastly thro' the drizzling rain On the bald street breaks the blank day.
> I have an informal proof that sqrt(2) is irrational:
> 1. Assume sqrt(2)=x/y, where x and y are nonzero integers and > relatively prime
2. Therefore x^2 and y^2 are nonzero integers and relatively prime (since no new prime factors are generated by squaring). 3. Therefore x^2 / y^2 is not an integer -- in particular, it is not 2. 4. Therefore assumption (1) is false -- there is no such x and y.
> 9. Therefore, sqrt(2) is irrational
> Btw, is there a less messy version of this?
This can be generalized from sqrt(2) to sqrt(n) where n is not already a perfect square.
> > I have an informal proof that sqrt(2) is irrational:
> > 1. Assume sqrt(2)=x/y, where x and y are nonzero integers and > > relatively prime > 2. Therefore x^2 and y^2 are nonzero integers and relatively prime > (since no new prime factors are generated by squaring). > 3. Therefore x^2 / y^2 is not an integer -- in particular, > it is not 2. > 4. Therefore assumption (1) is false -- there is no such x and y. > > 9. Therefore, sqrt(2) is irrational
> > Btw, is there a less messy version of this?
> This can be generalized from sqrt(2) to sqrt(n) where n is not > already a perfect square.
It could be further generalized to m-th roots of n.
In general, if x and y are naturals > 1 and relatively prime then x^m and y^n are relatively prime (m, n > 0).
