X-Message-Number: 4224 From: (Thomas Donaldson) Subject: Ettinger and Goedel fighting it out Date: Sun, 16 Apr 1995 18:36:25 -0700 (PDT) OK, so I found Ettinger's original message. It seems to me that he mistakes the activities of people like Goedel, but in his defense it's in a way that many popular commentators do also (though they don't go so far as he). Mathematics for some time has employed PROOFS. Proofs, whether or not the point is ever made explicitly in a particular case, can only be proofs within some kind of formal system. By showing the defects of any sufficiently large formal system, Goedel demonstrated that the entire Definition Theorem Proof scheme in which math is currently (still!) explained has some basic faults. That's all he demonstrated. And in fact that demonstration has some possible implications which lead us right into issues such as uploading. Proofs can be and have been put on computers. That whole pattern of thought is something which adapts to computers. What cannot be put on computers is our own VALUATION of a proof and VALUATION of the subject with which it deals (I'm not here saying that computers cannot be self-aware etc. I am saying that OUR valuation is what WE use to judge the WORTH of proofs). If, however, we wanted to computerize proofs, we should be aware that the computer (if capable of proofs with any hope of being significant to US) would also face a risk, in its plodding production of proofs, of never coming to an end with one particular proof. We would have to step in and stop the damn thing. Moreover, if it came to one of Goedel's "this statement is unprovable" statements, the poor thing would hang in yet another way. If you really want to design your computer to do this, you'd better give it a "RESET" button. It is the use of that formal system that is important here. Goedel's proof, whether seen as such or not, produced a severe criticism of the notion that math (and by implication, anything) could be neatly put into a nice formal system. To explain this point in ordinary language basically misses it, since our ordinary language is NOT a formal system, and many people have never been interested in proofs in the first place. I would even say that Goedel (though at the time there were hardly any computers worth the name) had come up with a problem of formalization in general. If our computer is to be able to operate on its own, then Goedel's proof gives us a few hints about what it must have not to come to a halt and need outside help. It is exactly because we human beings do NOT operate formally on axioms that we can succeed in surviving in the world. We have one kind of device which does that: neural nets. (If you wish to argue whether or not they are computers,you're welcome, but you're arguing about a definition. Note I said DEVICE). And so Goedel tells us a good deal by demolishing one particular idea about how we think. (And I do want to emphasize, as a mathematician, that we still follow the FORM of definitions and proofs, but as a mode of precise exposition rather than something in itself. And I can see even in mathematics a growth of other ideas for demonstrating some idea). Someday, of course, Goedel's demolition will seem quaint. No one would think of bothering to think that way. And so Goedel's Theorem will be forgotten. That is, of course, the general fate of negative results. Best and long long life, Thomas Donaldson Rate This Message: http://www.cryonet.org/cgi-bin/rate.cgi?msg=4224