, 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.,
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.,