View source for Logic for Computer Scientists/Modal Logic/Multimodal Logics – An example

==Multimodal Logics - An example==

If modal logics is to be used for expressing the knowledge of various agents,
one needs operators which are parametrised: we introduce box operators <math>[a]</math>,
which are paramtrised by arbitrary terms <math>a</math>; the same holds for <math>\langle a\rangle</math>,
the parametrised diamond operator.
<blockquote>
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."
</blockquote>

The following is a formalisation using the abbreviation <math>\square F</math>, which
stands for arbitrary nested paramtrised <math>[]</math>-operators. If we had only 2 wise
man <math>A</math> and <math>B</math>, <math>\square F</math> would stand for <math>[A]F \land [B]F \land [A][B]F \land [B][A]F \land [A][A]F \cdots </math>. Hence in general <math>\square F</math> stands for "<math>F</math> is
generally known".


<center>

<math>B \neq A \land C\neq A \land C\neq B</math>  the three wise are different <br><br>
<math>\square (w(A) \lor w(B) \lor w(C)) </math> it is generally known, that one of them has a
white spot <br><br>
<math>\square (\forall x,y: x\neq y \to (\lnot w(x) \to [y] \lnot w(x)))</math>  it is generally known,
that if someone has no white spot, the others know it <br>
<br>
<math>[C][B] \lnot [A] w(A) </math> C  knows, that B knows, that A does not know the colour of his spot <br><br>
<math>[C] \lnot [B] w(B)</math>   C knows, that B does not know the colour of his spot <br>
</center>



The theorem to be proven is "<math>C</math> knows that he has a white spot":
<center><math>
[C]w(c)
</math></center>


If we had a theorem prover for modal logics we could apply it to the above
specified  problem in order to obtain a proof and hence an explanation for the
theorem.

In the rest of this section we will introduce two methods for the definition of
such a theorem prover: A direct tableau calculus and a translation method in to
first order classical predicate logic.

{{BookCat}}