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.