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