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