Propositional modal logic

, syntactically, is simply the propositional calculus with the addition of the two modal operators and , 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 is a wff, then so are and .

At this point, we have the alphabet and grammar for . This system's semantical side is founded upon the notion of a Kripkean frame = (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., . 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 ; i.e., V assigns, to every atomic wff, the set of points at which it's true. Now, a model (the analogue to `interpretation' in our exposition of first-order logic) is simply a pair , V), and we can move on to define the key locution `formula is true at point w in model ', written

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

• iff for all w' such that wRw',
• iff there is a w' such that wRw', where

But what, many of our readers are no doubt asking, do and mean? What are they good for? One way to answer such questions is to read 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 .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 , where W denotes, still, the set of points. With rewritten to the more natural K, we say that K (`` knows '') is true at some point iff is true in every world such that 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 , and the last two are rules of inference.

K

T

4

5

Necessitation

From , infer K

Logical Omniscience (LO)

From and K infer K

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 White(A) K White(A)))
2. K (K (White(A) White(B)))
3. K K (White(B)))
4. White(A) K White(A)) 1, T
5. K (White(A) White(B)) 2,T
6. K (White(A)) K (White(B)) 5, K
7. (White(A)) K (White(B)) 4, 6
8. K (White(B)) White(A) 7
9. K K (White(B)) White(A)) 1-5, 8, LO
10. K K (White(B))) K (White(A)) 9,K
11. K (White(A)) 3,10