[FOM] The Lucas-Penrose Thesis
jmc at steam.Stanford.EDU
Fri Sep 29 17:51:28 EDT 2006
This is to extend the argument by Panu Praatika against the
Lucas-Penrose argument against human-level machine intelligence. It
also extends an argument I previously gave on FOM.
When a person thinks, at least Lucas or Penrose, of a computer program
doing mathematics, one tends to think of a program PA1 proving theorems in
a fixed axiomatic system, e.g. Peano arithmetic. If one is confident
of the consistency of PA, then one can readily give a true sentence
the program won't prove.
However, this is much too narrow a view of what we can program
computers to do. We can program the computer to regard PA as an
object, i.e. list its axioms and schemas. Then it can prove Goedel's
incompleteness theorems and exhibit a true sentence PA1 can't prove.
This is provided it believes in the truth of PA1.
We can do much more.
Here's a hypothetical dialog between Penrose and a computer
program taken from my review of "The Emperor's New Mind" in the
Bulletin of the American Mathematical Society, October 1990. [I
mistakenly dated it 1989 in my previous posting.]
Penrose: Tell me the logical system you use, and I'll tell
you a true sentence you can't prove.
Program: You tell me what system you use, and I'll tell you
a true sentence you can't prove.
Penrose: I don't use a fixed logical system.
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
Penrose: But the constructive ordinals aren't recursively
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.
If we want to write programs with the sophistication of human
mathematicians we have to go a lot farther than merely enough to
refute Lucas and Penrose. The programs will need to use a
language that matches the natural language text that ordinarily
surrounds the formal notation. It needn't match the syntax, but
it must admit the same kinds of vagueness that permeates
mathematical English. For example, my above use of "the
sophistication of human mathematicians" is somewhat vague, and
the programs will have to use equally vague locutions. Just
expressing the above formally as
Sophistication(Prog) >= Average(x,Sophistication(x),Mathematicians(x))
won't cure the vagueness of the predicate Sophistication. Humans
leave some terms vague, and I think programs will also have to
use somewat vague terminology.
Alas, the formalization of common sense language and reasoning
hasn't advanced far enough to match mathematical usage, let alone
that of (say) legal or literary usage.
More information about the FOM