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
We now say that
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.
Figure: Büchi automaton for .