[FOM] The Lucas-Penrose Thesis

[John McCarthy]

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
     ordinals.

     Penrose: But the constructive ordinals aren't recursively
     enumerable.

     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.