From: jqb@netcom.com (Jim Balter)
Date: Thu, 14 Nov 1996 01:55:29 GMT

In article <56dpd9$4gp@usenet.srv.cis.pitt.edu>,
Anders N Weinstein  wrote:
>In article , Jim Balter  wrote:
>>In article <328A2BEC.70E1@ix.netcom.com>,
>>be true, we cannot necessarily see the Godel sentence *as* true.  That is, if
>>presented with the Godel sentence, there is no reason to think that we will be
>>able to see that it is true, unless we can show that it *is* the Godel
>>sentence for that system.  And, just as we can "see" that Godel's theorem is
>>true (after all, it is a theorem), there are, contrary to popular belief,
>>formal consistent systems in which Godel's theorem can be derived (after all,
>>it is a theorem).
>
>Be careful to distinguish Godel's *theorem* from the Godel sentence
>used in the original proof. (Or *a* Godel sentence constructed for a
>particular system).

I was careful.  Each occurrence of "sentence" and "theorem"
above was intended, and intended to refer to two different things.

>One should also remember that a formal system is not an algorithm. The
>rules of a formal system themselves are "non-deterministic" and do not
>give a method for searching for proofs. Of course there are associated
>proof-enumerating algorithms that can be considered. 

There is an equivalence relation between Turing machines and algorithms.  Not
all Turing machines are methods for searching for proofs.  Whatever you mean
by "non-deterministic" above, it's a non-standard usage.
 
>In general, I think it takes quite a bit of work to know how to connect

No one said it was easy.

>the abstractions Godel's theorem dealt with, such as consistent formal
>systems, with flesh and blood human beings (or their brains). So it is
>very hard to derive an exciting conclusion about "mechanism" from it.
>For example, few people would committed to the claim that human beings
>instantiate consistent proof-enumerating algorithms.

Which is one reason why Lucas and Penrose are not worth bothering with.

>Of course, by the same token I think it is equally hard to derive any

No one said it was easy.

>substantive thesis from the slogan that "human beings are computers" or
>instantiate algorithms.  So one should be just as suspicious of the
>claim that we instantiate *inconsistent* proof-enumerating algorithms,

Proof enumeration is not to the point.

And not all suspicions are equally justified.

>>Totally wrong.  There are consistent systems that can derive Godel's theorem.
>>Nonetheless, they cannot derive their own Godel sentences.
>>Lucas does not show that we cannot be such a system.
>
>Although I think this is the wrong line of objection to Lucas/Godel (and
>you evidently think there are stronger ones) I will raise a question anyway. 

Wrong in what sense other than that it is questionable?

>I take it the Lucas response might be this: if you in some way
>instantiate a consistent formal system (whatever that might mean) then
>you could be presented with a Godelian proof using "your own" Godel
>sentence (i.e.  one constructed via Godel's technique for the system
>that is you).
>You read along, repeat the reasoning yourself, and then
>what? One would think, says our Lucas, you would come then to add G to
>the stock of things you believe about numbers and so transcend,
>angel-like, the limits of mechanism (Dennett).  Or do you expect to
>rather sputter, emit smoke, and explode, like computers in some
>movies?

Whatever a belief is, it is not a proof.  The question is what can I prove.
"I believe P but I cannot prove it" does not get to any sort of Godelian
contradiction.

>The real answer is that you would have to assume your own consistency
>as a premise in the reasoning process by which you come to add G to
>your stock of truths

Calling something a truth doesn't make it one.

>about numbers in the course of your reading.  And
>that leap of faith means engaging in some kind of reasoning not
>embraced by any formal system.

Calling it reasoning doesn't make it so.

If you want to equate beliefs with proven truths, then you will get an
inconsistent system.  But it isn't necessary to do so.  However, the point
isn't worth belaboring, because there is no reason to consider us to be
consistent systems.

--