next up previous
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 tex2html_wrap_inline773 tex2html_wrap_inline775 has the properties of both soundness and completeness.Let tex2html_wrap_inline797 be a set of first-order formulas, and tex2html_wrap_inline793 an arbitrary formula of this type. Then soundness consists in

displaymath1469

whereas completeness is

displaymath1471

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 ( tex2html_wrap_inline773 tex2html_wrap_inline861 , above) can be expressed by the two equations just given, as long as tex2html_wrap_inline1099 is understood to lack rules of inference for the quantifiers and tex2html_wrap_inline857 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 tex2html_wrap_inline797 of first-order formulas can deductively produce a given formula tex2html_wrap_inline791 . (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 tex2html_wrap_inline773 tex2html_wrap_inline861 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 tex2html_wrap_inline1489 is a function from the set of natural numbers N to tex2html_wrap_inline1489 . For example, the function

displaymath1493

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 tex2html_wrap_inline1499 . So for example the expression tex2html_wrap_inline1501 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 tex2html_wrap_inline967 on an infinite word tex2html_wrap_inline1507 , which is an infinite sequence

displaymath1509

such that

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

We now say that

Figure 1 shows a Büchi automaton for a certain language (specified in the caption).

  figure264
Figure: Büchi automaton accepting tex2html_wrap_inline765 .

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 tex2html_wrap_inline767 , 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 tex2html_wrap_inline791 the Büchi automaton tex2html_wrap_inline1545 corresponding to this formula, and then checks to see if there are strings accepted by tex2html_wrap_inline1545 . If so, then tex2html_wrap_inline791 is satisfiable; if not, tex2html_wrap_inline791 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.

  figure272
Figure: Büchi automaton for tex2html_wrap_inline767 .


next up previous
Next: Metatheory in a broader Up: Metatheory Previous: Metatheory

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