From: andersw+@pitt.edu (Anders N Weinstein)
Date: 14 Nov 1996 03:19:38 GMT
Organization: University of Pittsburgh
In article , Jim Balter  wrote:
>In article <56dpd9$4gp@usenet.srv.cis.pitt.edu>,
>Anders N Weinstein  wrote:
>
>>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.

I didn't mean a non-deterministic machine. Another term that is used is
"permissive" rules. 

The rules of chess do not determine a sequence of play (except in a few
cases of literally forced moves, e.g.  if only one move will get you
out of check). So the rules of chess do not define an algorithm for playing
chess. Rather they settle which transitions constitute correct play.

Similarly the axioms and inference rules of PM define what are correct 
proofs in the system. Unlike the rules of performing long division, they do 
not give an algorithm for finding a proof. The last is sometimes called
the "control problem" and PM leaves it open how to solve that. 

Many different deterministic algorithms might conform to the
"non-deterministic" rules of PM. It might be that human behavior is not
at all systematic or algorithmic, yet we might still claim that
mathematicians have a competence characterized by PM.

>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.

OK, but then you could just stick to this very short response: 

Godel's theorem gives us no rational basis at all for judging G is
true.  If we say so, it is only because we infer it from a non-rational
faith in the consistency of arithmetic.  So we cannot really do anything
computers can't do. Sure, the computer can't prove G, but neither can 
we (or Godel). We might prove the conditional that is Godel's theorem, 
but so can the computer.

That response (which has been floating around awhile, I believe it
occurs in an appendix to one of Putnam's early papers on functionalism)
seems to me to cut the Lucas argument off pretty damned quickly.