Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!samsung!sol.ctr.columbia.edu!bronze!chalmers From: chalmers@bronze.ucs.indiana.edu (David Chalmers) Newsgroups: comp.ai.philosophy Subject: Re: Minds, machines, and Godel Message-ID: <1991Jan19.055638.27731@bronze.ucs.indiana.edu> Date: 19 Jan 91 05:56:38 GMT References: <1991Jan18.203249.7022@sics.se> <1991Jan18.223602.15474@bronze.ucs.indiana.edu> <28154@cs.yale.edu> Organization: Indiana University, Bloomington Lines: 68 In article <28154@cs.yale.edu> mcdermott-drew@cs.yale.edu (Drew McDermott) writes: >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.] This is only one way to rewrite the TM as a formal system! First, a clarification: our TM is *judging* certain statements of first-order arithmetic, given to it as input, as true or false (and it may whirr forever on certain inputs if it wants to); it's not generating them. (The argument would still work with generation, but it would be more complex.) So the statements that the TM judges to be true are a recursively enumerable set. (More precisely, their Godel numbers form an r.e. set.) There is a fairly straightforward theorem that for any set of statements closed under logical consequence whose Godel numbers form an r.e. set, then that set of statements can be generated as the theorems of some formal system (from a decidable set of axioms). I think the theorem is due to Craig, you can certainly find it somewhere in Boolos & Jeffrey or any other standard text. It should be non-controversial that our set of statements is closed under logical consequence. Therefore the statements can be generated as precisely the theorems of some formal system. Sorry if this wasn't clear before. I thought that the relationship between recursive enumerability and axiomatizability was well known. >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. I'm assuming the TM is simulating an army of mathematicians working on judging the truth of a given statement. When they decide (after much checking and counter-checking) that the statement is certainly true, they lodge an irrevocable decision. (Some statements may be such that they never reach a decision; it doesn't matter.) So no retractions for our TM. >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. We need not specify such an N. It's allowed to run for an indefinite amount of time. The set of statements eventually recognized as true still form a recursively enumerable set. Recall that I'm idealizing away from the possibility of our army of mathematicians making mistakes in their final, considered decision. (And note that no-one is forcing them to make decisions on statements that they're not certain about. But certain statements, such as "2+2=4", or "first-order arithmetic is consistent" [actually its arithmetical analogue], will not be controversial.) I don't see any reason why this idealization is unreasonable. If, however, you want to dispute it, I can't provide a knockdown argument -- you can side with Minsky et al on the fundamentality of inconsistency. Either way, I don't see this deep conceptual incoherency and woolliness that you keep talking about. -- Dave Chalmers (dave@cogsci.indiana.edu) Center for Research on Concepts and Cognition, Indiana University. "It is not the least charm of a theory that it is refutable."