Path: utzoo!utgpu!news-server.csri.toronto.edu!bonnie.concordia.ca!thunder.mcrcim.mcgill.edu!snorkelwacker.mit.edu!apple!decwrl!shelby!neon!Neon!jmc From: jmc@DEC-Lite.Stanford.EDU (John McCarthy) Newsgroups: comp.ai.philosophy Subject: Re: Minds, machines, and Godel Message-ID: Date: 17 Jan 91 05:39:07 GMT References: <1991Jan16.035058.7465@bronze.ucs.indiana.edu> <91Jan16.135532edt.1132@neuron.ai.toronto.edu> <1991Jan17.040803.8205@bronze.ucs.indiana.edu> Sender: news@Neon.Stanford.EDU (USENET News System) Organization: /u/jmc/.organization Lines: 83 In-Reply-To: chalmers@bronze.ucs.indiana.edu's message of 17 Jan 91 04:08:03 GMT The following is taken from a review of the Penrose I wrote for the Bulletin of the American Mathematical Society, November 1990. 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 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 mathematics computer program. \noindent Penrose: Tell me the logical system you use, and I'll tell you a true sentence you can't prove. \noindent Program: You tell me what system you use, and I'll tell you a true sentence you can't prove. \noindent Penrose: I don't use a fixed logical system. \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. \noindent Penrose: But the constructive ordinals aren't recursively enumerable. \noindent Program: So what? You supply the extension and whatever confidence I have in the ordinal notation, I'll grant to the theory. If you supply the confidence, I'll use the theory, and you can apply your confidence to the results. [Turing adds to a system a statement of its consistency, thus getting a new system. Feferman adds an assertion that is essentially of the form $n(provable P(n)) nP(n)$. We've left off some quotes.] 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. Suppose we want a computer to prove theorems in arithmetic. We might choose a set of axioms for elementary arithmetic, put these axioms in the computer, and write a program to prove conjectured sentences from the axioms. This is often done, and Penrose's intuition applies to it. The G\"odel sentence of the axiomatic system would be forever beyond the capabilities of the program. Nevertheless, since G\"odel sentences are rather exotic, e.g. induction up to $\epsilon0$ is rarely required in mathematics, such programs operating within a fixed axiomatic system are good enough for most conventional mathematical purposes. We'd be very happy with a program that was good at proving those theorems that have proofs in Peano arithmetic. However, to get anything like the ability to look at mathematical systems from the outside, we must proceed differently. 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. Indeed the Boyer-Moore interactive theorem prover has been used by Shankar (1986) to prove G\"odel's theorem, although not in this generality. See also (Quaife 1988). 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. Many other mathematical, computer science and even philosophical problems will arise in such an effort.