next up previous
Next: Temporal logic Up: System Specification Previous: System Specification

Propositional modal logic

tex2html_wrap_inline773 tex2html_wrap_inline947 , syntactically, is simply the propositional calculus with the addition of the two modal operators tex2html_wrap_inline953 and tex2html_wrap_inline955 , which will be familiar to many readers. With the two new operators, of course, come newly admissible wffs, by way of the following straightforward formation rule:

If tex2html_wrap_inline791 is a wff, then so are tex2html_wrap_inline959 and tex2html_wrap_inline961 .
At this point, we have the alphabet and grammar for tex2html_wrap_inline773 tex2html_wrap_inline947 . This system's semantical side is founded upon the notion of a Kripkean frame tex2html_wrap_inline967 = (W, R), where W is simply a non-empty set (of points as Thayse 1989 says, or of possible worlds as it is often said), and R is a binary relation on W; i.e., tex2html_wrap_inline977 . R is traditionally called the accessibility relation. Now, let P contain all the atomic wffs generable from the logic's alphabet and grammar. We define a function V from P to tex2html_wrap_inline987 ; i.e., V assigns, to every atomic wff, the set of points at which it's true. Now, a model tex2html_wrap_inline991 (the analogue to `interpretation' in our exposition of first-order logic) is simply a pair tex2html_wrap_inline993 , V), and we can move on to define the key locution `formula tex2html_wrap_inline791 is true at point w in model tex2html_wrap_inline991 ', written

displaymath1003

The definition of this phrase for the truth-functional connectives parallels the account for first-order logic (e.g., tex2html_wrap_inline1005 iff it's not true that tex2html_wrap_inline1007 ). The important new information is that which semantically characterizes our two new modal operators, viz.,

But what, many of our readers are no doubt asking, do tex2html_wrap_inline955 and tex2html_wrap_inline953 mean? What are they good for? One way to answer such questions is to read tex2html_wrap_inline955 as `knows'. (An extensive catalogue of useful readings of the two operators is provided in Thayse 1989.) Such a reading very quickly allows for some rather tricky ratiocination to be captured in the logic. For example, Thayse 1989 has us consider the famous ``wise man puzzle'', which can be put as follows:

A king, wishing to know which of his three advisers is the wisest, paints a white spot on each of their foreheads, tells them the spots are black or white and that there is at least one white spot, and asks them to tell him the color of their own spots. After a time the first wise man says, ``I do not know whether I have a white spot.'' The second, hearing this, also says he does not know. The third (truly!) wise man then responds, ``My spot must be white.''

Thayse 1989 shows that the third wise man is indeed correct, by formalizing his formidable reasoning. The formalization (which is only given for the two-man version of the puzzle) starts with three propositions, viz.,

  1. A knows that if A doesn't have a white spot, B will know that A doesn't have a white spot.
  2. A knows that B knows that either A or B has a white spot.
  3. A knows that B doesn't know whether or not B has a white spot.
and proceeds to bring to bear on them the machinery of tex2html_wrap_inline773 tex2html_wrap_inline947 .In order to carry out the formalization, it is necessary to invoke a new set A of agents, and then broaden the accessibility relation R to a ternary relation tex2html_wrap_inline1061 , where W denotes, still, the set of points. With tex2html_wrap_inline955 rewritten to the more natural K, we say that K tex2html_wrap_inline1067 (`` tex2html_wrap_inline1069 knows tex2html_wrap_inline791 '') is true at some point tex2html_wrap_inline1073 iff tex2html_wrap_inline791 is true in every world tex2html_wrap_inline1077 such that tex2html_wrap_inline1079 The key axioms and rules needed to solve the puzzle are those from the propositional calculus (e.g., modus ponens), along with the following, where the first four are standard axioms of tex2html_wrap_inline773 tex2html_wrap_inline947 , and the last two are rules of inference.
K
tex2html_wrap_inline1085
T
tex2html_wrap_inline1087
4
tex2html_wrap_inline1089
5
tex2html_wrap_inline1091
Necessitation
From tex2html_wrap_inline1093 , infer K tex2html_wrap_inline1067
Logical Omniscience (LO)
From tex2html_wrap_inline1097 and tex2html_wrap_inline1099 K tex2html_wrap_inline1067 infer K tex2html_wrap_inline1103
Then the proof runs as follows (where the first three lines are symbolizations of the three propositions listed just above in the body of this paper):
  1. K tex2html_wrap_inline1105 White(A) tex2html_wrap_inline1107 K tex2html_wrap_inline1109 White(A)))
  2. K tex2html_wrap_inline1111 (K tex2html_wrap_inline1113 (White(A) tex2html_wrap_inline1107 White(B)))
  3. K tex2html_wrap_inline1105 K tex2html_wrap_inline1119 (White(B)))
  4. tex2html_wrap_inline1121 White(A) tex2html_wrap_inline1107 K tex2html_wrap_inline1109 White(A)) 1, T
  5. K tex2html_wrap_inline1113 (White(A) tex2html_wrap_inline1107 White(B)) 2,T
  6. K tex2html_wrap_inline1113 (White(A)) tex2html_wrap_inline1107 K tex2html_wrap_inline1119 (White(B)) 5, K
  7. tex2html_wrap_inline1121 (White(A)) tex2html_wrap_inline1107 K tex2html_wrap_inline1119 (White(B)) 4, 6
  8. tex2html_wrap_inline1121 K tex2html_wrap_inline1119 (White(B)) tex2html_wrap_inline1107 White(A) 7
  9. K tex2html_wrap_inline1105 K tex2html_wrap_inline1119 (White(B)) tex2html_wrap_inline1107 White(A)) 1-5, 8, LO
  10. K tex2html_wrap_inline1105 K tex2html_wrap_inline1119 (White(B))) tex2html_wrap_inline1107 K tex2html_wrap_inline1111 (White(A)) 9,K
  11. K tex2html_wrap_inline1111 (White(A)) 3,10


next up previous
Next: Temporal logic Up: System Specification Previous: System Specification

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