Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!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: <1991Jan17.170401.8536@bronze.ucs.indiana.edu> Date: 17 Jan 91 17:04:01 GMT References: <91Jan16.135532edt.1132@neuron.ai.toronto.edu> <1991Jan17.040803.8205@bronze.ucs.indiana.edu> Organization: Indiana University, Bloomington Lines: 82 In article jmc@DEC-Lite.Stanford.EDU (John McCarthy) writes: > The Penrose argument against AI of most interest to >mathematicians is that whatever system of axioms a computer is >programmed to work in, e.g. Zermelo-Fraenkel set theory, a man >can form a G\"odel sentence for the system, true but not provable >within the system. The Lucas/Penrose argument need not assume that the computer is working in any axiomatic system remotely like the standard systems of set theory and logic. All that is required is that it has a computational procedure for generating true statements of arithmetic. > The simplest reply to Penrose is that forming a G\"odel >sentence from a proof predicate expression is just a >one line LISP program. Imagine a dialog between Penrose and a >\noindent Program: I can use any system you like, although mostly >I use a system based on a variant of ZF and descended from 1980s >work of David McAllester. Would you like me to print you a >manual? Your proposal is like a contest to see who can name the >largest number with me going first. Actually, I am prepared to >accept any extension of arithmetic by the addition of >self-confidence principles of the Turing-Feferman type iterated >to constructive transfinite ordinals. The argument is not intended to apply to individual axiomatic systems that the program might use in an auxiliary fashion. Rather, it is intended to apply to the program as a whole (thus encompassing all of those systems if they are part of the system). > One mistaken intuition behind the widespread belief that >a program can't do mathematics on a human level is the assumption >that a machine must necessarily do mathematics within a single >axiomatic system with a predefined interpretation. I agree that this is a common misinterpretation, but the argument has broader scope. Assuming that the program is indeed a fixed finite program (of undetermined nature; the computations that go into determining the program's computation may look nothing like first-order logic or set theory, although it's not unlikely that such computations might occasionally be used), then the Godel argument applies. (It's a simple matter to convert any program into an "axiomatic" system that generates precisely the same statements. Then we call on Godel.) > Using a convenient set theory, e.g. ZF, axiomatize the >notion of first order axiomatic theory, the notion of >interpretation and the notion of a sentence holding in an >interpretation. Then G\"odel's theorem is just an ordinary >theorem of this theory and the fact that the G\"odel sentence >holds in models of the axioms, if any exist, is just an ordinary >theorem. Godelize the entire system. This will give a statement that it cannot generate which we can see to be true. > Besides the ability to use formalized metamathematics >a mathematician program will need to give credence to conjectures >based on less than conclusive evidence, just as human mathematicians >give credence to the axiom of choice. This is potentially closer to the point. If you hold that any system that humans use to determine mathematical truth is necessarily somewhat unreliable, then the TM that simulates the human may give rise to an inconsistent system, so that Godel's theorem will not apply. Of course humans are inconsistent in practice, but I'm not sure that I'd want a refutation of Lucas/Penrose to be based solely on this fact. At the very least you'd have to hold that's it's a *deep* and important fact about human competence (as opposed to some kind of noise in the system, a performance/competence distinction). Also it is relevant to realize that the argument applies equally to a simulation of the world's 100 best mathematicians working at determining the truth of a statement for 100 years, and only giving a yes/no answer when they are really sure (it's quite alright for them to say "don't know" for some). If you held that this system would be inconsistent, and that this inconsistency was a deep and important fact, then this could serve as the grounds for a refutation of the argument. I think, however, that a refutation of the argument should be based on something more clearcut than this. -- 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."