Slashdot Mirror
Towards a Wiki For Formally Verified Mathematics
An anonymous reader writes "Cameron Freer, an instructor in pure mathematics at MIT, is working on an intriguing project called vdash.org (video from O'Reilly Ignite Boston 4): a math wiki which only allows true theorems to be added! Based on Isabelle, a free-software theorem prover, the wiki will state all of known mathematics in a machine-readable language and verify all theorems for correctness, thus providing a knowledge base for interactive proof assistants. In addition to its benefits for education and research, such a project could reveal undiscovered connections between fields of mathematics, thus advancing some fields with no further work being necessary."
Skynet approves of this machine readable knowledge store.
So Godel proved that Russell was wrong, then?
1. Russell did not, as far as I know, write any proofs in machine-readable language.
2. Goedel proved that such an endeavor cannot contain all true statements. But of course they never claimed that it would.
Maybe if you paid more attention you would be less amazed.
If you mod me Overrated, you are admitting that you have no penis.
Silicon Jedi,
For invoking the name "Godel" as if it meant anything in this context when it clearly doesn't, your Slashdot posting license is hereby revoked for a period of one year. The Court also sentences you to read what Godel actually wrote. Furthermore, after your posting license is returned, the Court imposes a probationary period of 3 years during which you will be required to think and apply logic to your posts before you click Submit.
Next case!
If you mod me Overrated, you are admitting that you have no penis.
I'm no more of a mathematician than you are, but I've had the chance to discuss this with people who really do understand it. Your description is, I think, correct, but not your conclusion. What Goedel proved was not that such an endeavor was impossible, but that it could not be complete. This is because in any system sufficiently advanced to be interesting, there would always be some things that were true but which couldn't be proven to be true. (There would also, BTW, be things that were false but couldn't be shown to be false.)
Good, inexpensive web hosting
I don't know, all I know is that I have never been more tempted to vandalize a Wiki, in this case by replacing the middle steps of as many proofs as possible with "And then a miracle occurs..."
The enemies of Democracy are
It's a pretty much work. A lot of 'obvious' English sentences translate to bulky code for proof verifier.
Just look at the definition of Peano arithmetic, for example: http://pauillac.inria.fr/coq/V8.1/stdlib/Coq.Arith.Plus.html
Hey. A lot of people devote a lot of their time in explaining their areas of mathematics to the general public (including myself). And as for your distaste for abstraction. That's what maths is! There is a reason the general public do not follow much in the way of mathematical developments and that is because research level mathematics is actually really hard and takes a lot of dedication to understand well. There is also no elitist clique. We love it when people show interest in our work and want to understand it.
Very close. To be 100% correct though, Goedel proved that any such endeavor would either be incomplete, or self-contradictory. In other words, for any sufficiently advanced system, there will be some things that are true but which can't be proven to be true within the system, or else there will be some things which can be proven to be true within the system but which can also be proven to be false within the system.
My apologies. [I had to brush up on the actual numbering system].
Correction: The Godel numbering system assigned a unique prime number to each symbol and axiom of his arithmetic. Then, the IDs of the combinations of symbols making up formulas were computed by raising each symbol or axiom ID to the power of its position in the sequence. And, finally, the ID of each proof or theorem by applying the same algorithm to the formula IDs making up each proof. More info here.
"Goedel, Escher, Bach" is an absolutely astonishing book about this subject, and the foundations of logic in general. Applications to AI are also discussed. Admittedly, I had to stop reading it since it rather messed my head up (Got about 3/4 through and couldn't stop dreaming about maths). Highly recommended for any self-respecting geek.
http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach
Slashdot: news for Apple. Stuff that Apple.
I like the following elementary presentation I picked up from prof. M. Stanley at SJSU:
A first order axiomatic theory can have any three of the following, but not all four:
(1) Be recursively axiomatizable, i.e. a computer program can decide the set of axioms.
(2) Be expressive enough to capture all the basic facts about arithmetic.
(3) Be consistent, i.e. not allow to derive a contradiction.
(4) Be complete, i.e. for any statement F, prove either F or (not F).
I am a mathematician and in fact one who works in this area and what you say is pretty much correct.
More accurately what Godel showed is that no system complex enough to include arithmetic with a computable proof predicate is complete.
Let's take this apart and see what it means.
More precisely the system must be sufficiently strong to prove a few basic facts about the integers and not prove false things about the integers.
-------------
People tend to make this whole thing way harder than it is. Here is a quick paragraph long sketch of Godel's first incompletness theorem.
Suppose there is a predicate P(s,p) which holds whenever p is an integer coding for a proof of the statement coded by the integer s (if you sit down for a few minutes you can figure out how to do the coding). Now suppose that P(s,p) can be expressed by a sentence in number theory involving only an existential quantifier, e.g, P(s,p) Ez(blah holds of s, p) where blah has no quantifiers.
Now it turns out that if you are a bit clever you can show that there is a sentence G so that
G holds iff (Ep)P('~G',p)
Where 'G' denotes the integer that codes for the sentence G. In other words G says "There is a proof that this statement is false".
Now suppose there was a proof of G. In this case it must follow that since the system correctly interprets arithmetic that there really is a proof of the negation of G. Hence both G and ~G have proofs so the system is incomplete. But if there was a proof of ~G then, as the system correctly interprets arithmetic, there is no proof of ~G. This is a contradiction. So neither G or ~G have a proof.
---------
The only hard part here is showing that G can talk about itself. The formal proof is pretty straightforward if we leave out the details. We define a formula F(n) (where n is a free variable) defined by:
Now consider the formula F('F'), i.e. apply F to the integer that codes for F. Expanding out the definition we see that
So we get our G simply by setting G = F('F'). To get an understanding about where you might get the idea to define F as this you need to understand that existential statements are really program and that this is really an application of the recursion theorem.
If you liked this thought maybe you would find my blog nice too:
Godel proved that Peano arithmetic is incomplete. There are some axiomatic systems that are both consistent and complete. Examples of such systems include plane Euclidean geometry and Presburger arithmetic.
Here are more examples:
http://en.wikipedia.org/wiki/Complete_theory