Difference between informal and formal proofs?
Protoman
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!
Balthasar
<Protom...@gmail.com> wrote:
>
> 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 seeing such proofs you might check:
http://us.metamath.org/
>
> This is an informal proof, but what's the formal proof?
>
You might check Matamath for one.
You also might like to read:
Freek Wiedijk: "Short explanation of why I'm coding a proof of the
Jordan curve theorem"
http://www.cs.ru.nl/~freek/jordan/index.html
B.
--
"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)
PiperAlpha167
> 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.
Frederick Williams
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.
herbzet
Protoman wrote:
[...]
> 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.
--
hz
herbzet
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).
--
hz