Logic for Computer Scientists/Modal Logic/Multimodal Logics – An example
Multimodal Logics - An example
editIf modal logics is to be used for expressing the knowledge of various agents, one needs operators which are parametrised: we introduce box operators , which are paramtrised by arbitrary terms ; the same holds for , the parametrised diamond operator.
![{\displaystyle [a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea82bc70a8e322f13a3c4e5b9d5d69e8ef097ad8)
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."
The following is a formalisation using the abbreviation , which stands for arbitrary nested paramtrised -operators. If we had only 2 wise man and , would stand for . Hence in general stands for " is generally known".
![{\displaystyle []}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0261e8d17bc0832139076efdad67e7c0abf21cff)
![{\displaystyle [A]F\land [B]F\land [A][B]F\land [B][A]F\land [A][A]F\cdots }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba2a70a5beb897c28125913c29ce6d7bb3649543)
the three wise are different
it is generally known, that one of them has a
white spot
it is generally known,
that if someone has no white spot, the others know it
C knows, that B knows, that A does not know the colour of his spot
C knows, that B does not know the colour of his spot
![{\displaystyle \square (\forall x,y:x\neq y\to (\lnot w(x)\to [y]\lnot w(x)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0940dd8e2552adae0b42a2f66ed8bfd5fd7ce42e)
![{\displaystyle [C][B]\lnot [A]w(A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9630849e34209aa28a1941b36a7a965cba012353)
![{\displaystyle [C]\lnot [B]w(B)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2bd6651c3a4890a2493aada50b514976e34807b0)
The theorem to be proven is " knows that he has a white spot":
![{\displaystyle [C]w(c)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2c2d0dc681e3f4c75c55766c4427842b3e873a0c)
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.