Gödel, Escher, Bach An Eternal Golden Braid by Douglas R. Hofstadter

human intellect, and the computer has been employed, with more or less

ingenuity, as a tool for realizing an idea devised by the human. The pro-

gram which carries this out is not anything which we can identify with. It is

a simple and single-minded piece of software with no flexibility, no

perspective on what it is doing, and no sense of self. If and when, however,

people develop programs which have those attributes, and pieces of music

start issuing forth from them, then I suggest that will be the appropriate

time to start splitting up one's admiration: some to the programmer for

creating such an amazing program, and some to the program itself for its

sense of music. And it seems to me that that will only take place when the

internal structure of such a program is based on something similar to the

"symbols" in our brains and their triggering patterns, which are responsible

for the complex notion of meaning. The fact of having this kind of internal

structure would endow the program with properties which would make us

feel comfortable in identifying with it, to some extent. But until then, I will

not feel comfortable in saying "this piece was composed by a computer".

Theorem Proving and Problem Reduction

Let us now return to the history of AI. One of the early things which people

attempted to program was the intellectual activity of theorem proving.

Conceptually, this is no different from programming a computer to look

for a derivation of MU in the MIU-system, except that the formal systems

involved were often more complicated than the MIU-system. They were

versions of the Predicate Calculus, which is an extension of the Proposi-

tional Calculus involving quantifiers. Most of the rules of the Predicate

Calculus are included in TNT, as a matter of fact. The trick in writing such

a program is to instill a sense of direction, so that the program does not

wander all over the map, but works only on "relevant" pathways-those

which, by some reasonable criterion, seem to be leading towards the de-

sired string.

In this book we have not dealt much with such issues. How indeed can

you know when you are proceeding towards a theorem, and how can you

tell if what you are doing is just empty fiddling? This was one thing which I

hoped to illustrate with the MU-puzzle. Of course, there can be no defini-

tive answer: that is the content of the limitative Theorems, since if you

could always know which way to go, you could construct an algorithm for

proving any desired theorem, and that would violate Church's Theorem.

There is no such algorithm. (I will leave it to the reader to see exactly why

this follows from Church's Theorem.) However, this doesn't mean that it is

impossible to develop any intuition at all concerning what is and what is not

a promising route; in fact, the best programs have very sophisticated

heuristics, which enable them to make deductions in the Predicate Calculus

at speeds which are comparable to those of capable humans.

The trick in theorem proving is to to use the fact that you have an

overall goal-namely the string you want to produce-in guiding you

locally. One technique which was developed for converting global goals

Artificial Intelligence: Retrospects 609