The first interesting metatheoretical result that
students of LAI are likely to assimilate is that which implies that
has the properties of both soundness and
completeness.Let 
be a set of
first-order formulas, and 
an arbitrary formula
of this type. Then soundness consists in
whereas completeness is
For an excellent Henkin-style proof of completeness, see Ebbinghaus et
al. 1984
(the original proof is due to Gödel).
The soundness and completeness of the propositional calculus
( 
, above) can be expressed by the two equations
just given, as long as 
is understood to lack rules of inference
for the quantifiers and 
is understood in the
``truth-table'' sense. The next significant metatheoretical
result usually presented concerns decidability: First-order logic
is not decidable; i.e., there is no algorithm for determining whether or
not a first-order formula is valid and, hence, no algorithm for determining
whether or not a given set of first-order formulas can
deductively produce a given formula 
. (The propositional
calculus, on the other hand, is decidable: There is an algorithm
(which can simply construct a truth-table)
that can tell if a wff of is true on all truth-value
assignments.)
There are many results along these lines in the volumes under
review. Our favorite cluster of such results concerns the decidability
of the linear-time temporal logic we considered above. The decision procedure
for this logic
is a fascinating one that views formulas in the logic as infinitely
long strings and then proceeds to classify such strings with help from
a variant on finite-state automata - Büchi automata - which ``accept''
them.One of us (Selmer) has had much success teaching temporal
logic with help from Büchi automata (a number of examples of such
automata reside on his web site, under the course Symbolic Logic).
Students generally find the decision procedure interesting; here are
some of the details:
An infinite word on an alphabet 
is a function from the set of
natural numbers N to . For example, the function
is the infinite word wherein a and b alternate forever. To represent
sets of infinite words, we extend regular expressions
(with which many readers will be familiar) by way of
the infinite repetition operator 
. So for example the
expression 
represents the set of words containing only
the infinite word w(n) seen above.
Büchi automata, whose
``architectural'' elements are simply those
of finite state automata (FSAs), can be used to define sets of infinite words,
as follows.
The first
concept needed for such a definition is that of an execution of
an FSA 
on an infinite word 
, which is an infinite
sequence
such that
, is an initial state;
is obtained from the previous
one in accordance with the transition function of the FSA .
We now say that
is accepting iff there is some accepting state
s and an infinite number of integers i such that 
);
is the set of all infinite words accepted by .
Figure 1 shows a Büchi automaton for a certain language (specified in the caption).
Figure: Büchi automaton accepting 
.
The key idea in moving from formulas of linear time temporal logic to
their corresponding Büchi automata is that such formulas can be viewed
as true on certain infinite histories.
For example, the formula 
, recall,
is true of every history in which p is eventually true; so the Büchi
automaton is the one seen in Figure 2. In this flow graph, acceptance happens
only if the accept state (the double circle)
is ``hit'' infinitely many times. But that cannot be accomplished unless p
is hit at least once; i.e., acceptance happens only if p is eventually hit,
and then history moves on forever, with the question of whether p remains true or
becomes true again left as an open question. The algorithm
for deciding whether or not a formula
from linear-time temporal logic is satisfiable first generates from a formula
the Büchi automaton 
corresponding to this formula, and
then checks to see if there are strings accepted by . If so, then
is satisfiable; if not, is not
satisfiable.Complexity-theoretic
results should be included under the ``normal sense'' of
metatheory. An interesting paper in this area is ``Hard Problems for Simple
Default Logics'', by Henry Kautz and Bart Selman (in Brachman et al.),
which shows that some
aspects of default reasoning
are suprisingly complex and some suprisingly easy.
