Modern first-order logic (denoted, hereafter, following tradition, by ` ') is the cornerstone of any respectable exposition of LAI; we give here a quick review of it in accordance with Glymour's Chapter 6 (``Symbolic Logic'') and Thayse's 1989, Chapter 1 (``Languages and Logic''):Thayse 1989 provides a more mathematically detailed account than Glymour, which isn't surprising: Glymour's intended audience is students in introductory philosophy courses. (Susan Russinoff (1995) claims that Glymour is too advanced for such introductory courses, because the students in question may have no background in logic, probability theory, or computability theory. We have found at Rensselaer, however, that Glymour is a remarkably effective text for Introduction to Philosophy.)
Given an alphabet (of variables ; constants ; n-ary relation symbols ; functors ; quantifiers ; and the familiar truth-functional connectives ( ), one uses standard formation rules (e.g., if and are well-formed formulas (wffs), then is a wff as well) to build ``atomic'' formulas and then more complicated ``molecular'' formulas. >From sets of these formulas (say ), given certain rules of inference (e.g., modus ponens: from and , infer ), individual formulas (say ) can be inferred; such a situation is expressed by meta-expressions like . First-order logic includes a semantic side that systematically provides meaning for formulas involved. In first-order logic, formulas are said to be true (or false) on an interpretation, often written as . (This is often read, `` satisfies '', or `` models (or is a model of) ''.) For example, the formula might mean, on the standard interpretation for arithmetic, that for every natural number n, there is a natural number m such that m > n. In this case, the domain of is N, the natural numbers, and G is the binary relation ; i.e., > is a set of ordered pairs (i, j), where and i is greater than j. Some formulas of are valid, in the sense that they are true on all interpretations. For example, any formula of the form is valid; such a fact is customarily written . A formula that is true on at least one interpretation is satisfiable.
It is easy enough to generalize from this account to the broader concept of a logical system, and doing so is crucial for understanding LAI and the six books under consideration.Because, in the context of explicating LAI (and, for that matter, CAI), it's necessary to include syntactic, semantic, and proof-theoretic elements, our account of logical system is somewhat broader than the standard account that figures in (say) Lindström's Theorems. For the narrower account, as well as a nice presentation of these theorems, see Ebbinghaus et al. 1984. It's perhaps worth pointing out that semiotic systems may be justifiably regarded to be generalizations of logical systems. For a brief introduction to semiotic systems in the context of AI, see Fetzer 1994. A logical system includes an alphabet (the symbols from which well-formed formulas are to be built); a grammar specifying how wffs are to be generated; a semantic relation, a binary relation (e.g., as presented in the previous paragraph) holding between interpretations (or other structures designed to formally model aspects of ``reality'') and formulas; and a proof theory that makes precise how reasoning in the system is to proceed.
It is also usually important that a logical system have associated with it a metatheory, which would address questions such as whether the system in question is sound, complete, decidable, and so on. Such metaproperties are determined by bringing mathematical tools to bear on the system in question.
To anchor things a bit, consider first a system even simpler than first-order logic, viz., the propositional calculus, , a familiar and simple logical system, and one introduced in solid fashion in Thayse 1989.This is as good a place as any to point out that there is in fact a volume, Thayse 1989a, that precedes Thayse 1989, with nice coverage of most of elementary logic and logic programming. Thayse 1989a isn't reviewed herein. has for an alphabet propositional variables , and the truth-functional connectives; its grammar is the grammar of without rules covering the quantifiers; its semantics are based on truth-tables (so that, e.g., holds iff is true on every truth-value assignment in an exhaustive truth-table for ); and the proof-theory of can be given by familiar natural-deduction rules (e.g., modus ponens). Another logical system, this one ``beyond'' , is second-order logic, , which adds relation variables , to the alphabet of , which in turn allows (via the associated grammar) for formulas expressing such things as Leibniz's Law (two things are identical iff they have precisely the same properties):
Of course, logical systems are mathematical creatures. How does LAI end up with working programs? Suppose that we want to implement a logical system able to play the role of a guidance counselor in advising a high school student about which colleges to apply to. And suppose that we want to essentially work in . The first thing we need to do is create an ontology of the domain in question; accordingly, we may posit categories that include SATs, small liberal-arts colleges, national universities, grade-point averages, etc. All of these things must be representable by symbols from, and strings over, an alphabet of our devising (though part of the alphabet is unalterable; e.g., we know that we have the quantifiers). To focus the situation, suppose that we want a rule in such a system that says ``If a student has low SATs and a low GPA, then none of the top twenty-five national universities ought to be applied to by this student.'' Assume that we have the following interpreted predicates: Sx iff x is a student, for x has low SATs, for x has a low GPA, Tx for x is a top-twenty-five national university, and Axy for x ought to apply to y. Then the rule in question, in first-order logic, becomes
Let's suppose, in addition, that Steve is a student denoted by the constant s in the system and that he, alas, has low SATs and a low GPA. Assume also that v is a constant denoting Vanderbilt University (which happens to be a top twenty-five national university according the U. S. News & World Report's annual rankings). These facts are represented in the system by
Our implemented logical system, based as it is on first-order logic, can verify
that is, it can deduce that Steve ought not to apply to Vanderbilt.
At this point, we have identified, with respect to LAI, the following four fundamental categories: historical, philosophical, and mathematical foundations; creation and specification of logical systems themselves; metatheory; and ways of getting to an implementation. Given these categories, our books fall out as indicated in Table 1, where we have a range from 0 for ``no coverage'' to 1 for ``much coverage''.
Table 1: Breakdown of Coverage under Four Fundamental Categories
The remainder of the paper consists of selected discussion, via our six books, of these four categories, and then one final, brief section centered around a thought-experiment designed to display one of LAI's matchless virtues.