   Next: Metatheory in a broader Up: Metatheory Previous: Metatheory

## Metatheory in the standard sense

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

1. the first state of an execution, , is an initial state;
2. each state of the sequence is obtained from the previous one in accordance with the transition function of the FSA .

We now say that

• an execution of a Büchi automaton is accepting iff it contains some accepting state an infinite number of times (i.e., an execution is accepting iff there is some accepting state s and an infinite number of integers i such that );
• a word w is accepted by a Büchi automaton iff there exists an accepting execution of that automaton on that word; and
• the language accepted by a Büchi automaton 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. Figure: Büchi automaton for .   Next: Metatheory in a broader Up: Metatheory Previous: Metatheory

Selmer Bringsjord
Mon Nov 17 14:57:06 EST 1997