MINDS, MACHINES AND GÖDEL
J. R. LUCAS
GöpeL's Theorem seems to me to prove that Mechanism is false, that is, that minds cannot be explained as machines. So also has it seemed to many other people: almost every mathematical logician I have put the matter to has confessed to similar thoughts, but has felt reluctant to commit himself definitely until he could see the whole argument set out, with all objections fully stated and properly met. This I attempt to do.
Gödel's theorem states that in any consistent system which is strong enough to produce simple arithmetic there are formulae which cannot be proved-in-the-system, but which we can see to be true. Essentially, we consider the formula which says, in effect, "This formula is unprovable-in-the-system". If this formula were provable-in-the-system, we should have a contradiction: for if it were provable-in-the-system, then it would not be unprovable-inthe-system, so that "This formula is unprovable-in-the-system" would be false: equally, if it were provable-in-the-system, then it would not be false, but would be true, since in any consistent system nothing false can be proved-in-the-system, but only truths. So the formula "This formula is unprovable-in-the-system" is not provablein-the-system, but unprovable-in-the-system. Further, if the formula. "Thisformula is unprovable-in-the-system" is unprovable-in-thesystem, then it is true that that formula is unprovable-in-the-system, that is, "This formula is unprovable-in-the-system" is true.
The foregoing argument is very fiddling, and difficult to grasp fully: it is helpful to put the argument the other way round, consider the possibility that"This formula is unprovable-in-the-system" might be false, show that that is impossible, and thus that the formula is true; whence it follows that it is unprovable. Even so. the argument remains persistently unconvincing: we feel that there must be a catch in it somewhere. The whole labour of Gödel's theorem is to show that there is no catch anywhere, and that the result can
A paper read to the Oxford Philosophical Society on October 3o, 1959. See A. M. Turing: "Computing Machinery and Intelligence": Mind, 19so. pp. 433-6o, reprinted in The World of Mathematies. edited by James R. Newman, pp. 2o99-123: and K. R. Popper: "Indeterminism in Quantum Physics and Classical Physics": British Journal for Philosophy of Science. Vol. I (19s1), pp. 179-88. The question is touched upon by Paul Rosenbloom; Elements of Mathematical Logic; pp. 2o7-8; Ernest Nagel and James R. Newman; Godel's proof, pp. 1oo—a; and by Hartley Rogers; Theory of Recursive Functions and Effective Computability (mimeographed), 1957. Vol. I. pp. 15a ff.
1961 年 Unimation 公司生产了世界上首部工业机器人“ Unimate”，应用于通用汽车总装线上。
408
附录 人工智能历史大事记