Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!yale!cs.yale.edu!mcdermott-drew
From: mcdermott-drew@cs.yale.edu (Drew McDermott)
Newsgroups: comp.ai.philosophy
Subject: Re: Minds, machines, and Godel
Message-ID: <28154@cs.yale.edu>
Date: 19 Jan 91 04:43:37 GMT
References: <1991Jan18.191303.6840@bronze.ucs.indiana.edu> <1991Jan18.203249.7022@sics.se> <1991Jan18.223602.15474@bronze.ucs.indiana.edu>
Sender: news@cs.yale.edu
Organization: Yale University Computer Science Dept., New Haven, CT 06520-2158
Lines: 87
Nntp-Posting-Host: aden.ai.cs.yale.edu
Originator: dvm@aden.CS.Yale.Edu


   In article <1991Jan18.184116.5299@bronze.ucs.indiana.edu> chalmers@bronze.ucs.indiana.edu (David Chalmers) writes:
   >In article <28145@cs.yale.edu> mcdermott-drew@cs.yale.edu (Drew McDermott) writes:
   >
   >>I dispute that Godel ever proved anything about this broad class of
   >>Turing machines.  This class includes systems that are *mistaken*
   >>about mathematics to some degree, for instance.  Or systems that
   >>change their minds.  If you rule such Turing machines out, then you've
   >>simply begged the question whether human mathematicians are Turing
   >>machines, because people do indeed change their minds, and can indeed
   >>be mistaken about some parts of mathematics while being quite
   >>competent at other parts.
   >
   >As I've said a number of times, I'm idealizing away from inconsistency,
   >because I don't think that inconsistency is the root of the problem.  You
   >may disagree.
   >

Forget inconsistency; being mistaken does not entail being
inconsistent.  Changing one's mind can't be modeled at all within
formal arithmetic.  Neither is being led to a proof by an apple
falling on one's head (or touch sensor).

   >Given that step, then take our TM that simulates the judgment of a
   >mathematician (or an army of mathematicians).  Convert it straightforwardly
   >to an axiomatic system that generates precisely those statements of
   >first-order arithmetic that the mathematicians judge to be true.  

This step is not straightforward!  I know what you're alluding to: the
usual transformation of a Turing machine into a term-rewriting system.
The problem with that construction in this context is that a Turing
machine that we interpret as telling us mathematical conjectures will
not get transformed into a formal system for generating conjectures in
the same domain.  Instead, it will get transformed into some
completely uninteresting system of Turing-machine state descriptions.  
[I should acknowledge Marvin Minsky for pointing this out to me years
ago; evidently, he should have pointed it out to more people.]

Let's grant that idealization is a good thing, and assume that our TM
mathematician does nothing but print out its conclusions, without ever
communicating with other mathematicians.  One plausible design for
this system is to have it employ various techniques of varying degrees
of soundness for arriving at these conclusions.  (E.g., the use of
diagrams; naive set theory). If a conclusion seems to withstand all
attempts to disprove it, it gradually becomes accepted, and the TM
prints it out.  If a counterexample or a fallacy in the proof later
becomes apparent, it prints out a retraction.

One might object that this would be an untrustworthy mathematician.
Well, so are people.

One might object that one couldn't build such a TM.  But that begs the
original question.  We're assuming you can, supposedly in order to get
a contradiction.

So let's assume that such a mathematician can be built.  Please note
that *we can still perform the usual transformation of this Turing
machine into a proof system.*  There is more than one way to do it.
If we want to have a system that generates all and only the states the
machine can reach, then the proof system's language will be a language
for describing machine and tape configurations.  This language will
just not be about mathematics at all.  

On the other hand, if we choose to axiomatize "conclusions the machine
reaches after N state transitions," for some N, then let's suppose
that also can be made into a formal system.  Unfortunately, the resulting
system is not sound.

Hence we have a choice between modeling the Turing machine as a formal
system that says nothing about mathematics, or viewing it as an
unsound formal mathematical system.  Either way, Godel's argument does
not apply.

   >
   >>At this point, I'd like to see what Chalmers considers the definitive
   >>refutation of the "Mind, Machines, and Godel" argument.
   >
   >I think that the correct refutation is tied up with the question of how we
   >"see" that certain systems are consistent, and the arguments by Torkel
   >Franzen are coming close to that point, although even there the argument has
   >at least temporary defenses.  

I like Franzen's argument.  I like McCarthy's too.  It's not
surprising that an argument cobbled together from misunderstood
fragments of several theorems has several refutations.

                                             -- Drew McDermott