When it comes to the history of AI, there may be no more
informative book, ounce for ounce, than
Glymour; certainly it would be difficult to find one stocked
with as much cocktail-party ammunition.
What thinker first articulated a serious (= genuinely rigorous) version
of the AIish doctrine that the mind is a computational system?
Did you answer ``Hobbes'' or ``Leibniz''? Those, as Glymour explains, are
not indefensible answers. But, as Glymour informs us, it was really
Carnap, via his 1929
*The Logical Construction of the World*, who first
expressed, in a form suitable, in principle, for capture in (say) Lisp,
the vision that the mind is a program. All of this, we grant, may be
knowledge possessed by cognoscenti--but even they, we wager, will be
surprised to learn that it was the colorful philosopher Ramon Lull who first
planted the computationalist seeds that flowered into Leibniz's dream
for a ``calculus of thought'' and
Hobbes's conviction that thinking is mere ``calculation''.
Lull? That's right. As we read in Glymour:

[Lull] spent his time with games and pleasantries and is reputed to have made great efforts to seduce the wives of other courtiers. Accounts have it that after considerable effort to seduce a particular lady, she finally let him into her chambers and revealed a withered breast. Taking this as a sign from God, Lull gave up the life of a courtier and joined the Franciscan order. (p. 70.)

As Glymour explains, not long after
his singular repentance, Lull had built certain
*machines* that he believed could be used to demonstrate to Moslems
the truth of Christianity. Hidden in these intricate devices
(which were composed of disks with common
spindles displaying letters standing for
Latin words signifying divine attributes)
is the notion that reasoning can be mechanical and that it can be based on
representations more robust than that expressible in
Aristotle's theory of the syllogism.

We should point out that Glymour's historical discussion
revolves around a record of attempts to answer the question
``What is a proof?''--a question that the likes of
Aristotle, Leibniz, and Boole failed to answer.
It was Frege, the man Glymour rightly says ``stands to logic
as Newton stands to physics'' (p. 120),
who finally cracked the puzzle; his work led directly to
the orthodox answer, namely that a proof is that which can
be formalized as a derivation in first-order logic.By our lights,
for what it's worth, classical mathematics includes truths that can only
be formalized in logical systems *beyond* first-order logic.
This isn't
the place to press this point--but perhaps there's space to at least
get the point on the table: Consider the
fact that beliefs about, say, Goldbach's Conjecture
(every even number 4 is the sum of two primes) are plausibly regarded
to be part of classical mathematics--since a student of number theory
ought to receive, as part of her education, information about what
mathematicians believe about Goldbach's Conjecture.
To formalize propositions of the form
`Agent *s* believes proposition *p*', it seems necessary to go beyond
first-order logic.

Mon Nov 17 14:57:06 EST 1997