Finishing my Modal Logic course at FCT-UNL, I was still wondered about the reality of applying Modal Logic into real application. However, the 4th class on Nonclassical Logics at TUW somehow gave me the idea of using Modal Logic to formalize agents' knowledge and made me really excited. While reviewing the materials, I was a bit confused, then discussions with Prof. Fermueller has made it clearer, and me, more interested in Modal Logic in particular. Let's see what was the confusion here and how it was clarified.

(This entry requires you the fundamentals of Modal Logic, such as the semantics of $\Box$ and the system S5)

Let's say we have a finite set of agents 1,...,n. For each agent i, there is a modal operator $K_i$ with the following intended interpretation:

$K_iA$ means "Agent i knows that A". Notice that $K_i$ is actually the modal operator $\Box$. By using letter K, we want to emphasis the "Known" meaning of the operator. So, $K_iA$ iff $\mathcal{M},w^*\models A$ for all world $w^*$ such that $wR_iw^*$.

Now we need to find a system to guarantee all the principles of modeling knowledge, which are:

1. Distribution axiom: $(K_iA\land(K_i(A\supset B))\supset K_iB$ [internalize modus ponens]
2. Knowledge generalization rule: If A is valid then also $K_iA$ is valid
3. Knowledge axiom: $K_iA\supset A$ [only facts can be known]
4. Positive introspection: $K_iA\supset K_iK_iA$ [an agent knows that she knows what she knows]
5. Negative introspection: $\neg K_iA\supset K_i\negK_iA$ [an agent knows that she doesn't know what she doesn't know]

S5 was shown by a theorem that it is in fact the smallest normal modal logic that includes the knowledge axiom as well as positive and negative introspection. With S5, we have: reflexive, symmetric and transitive properties. Hence it follows from the soundness and completeness of S5 that each accessibility relation of a corresponding frame is an equivalent relation. Therefore, we will simplify the diagram by representing each equivalent relation by a line segment between two worlds instead of drawing the loops for reflexivity and left-right arrows for symmetry. To be more specific, the following two diagram are equal:

Attach:Minh/Uploads/ML-equivalent-representation.jpg Δ

Then we come up with an equivalence class of the equivalence relation $R_i$ which consists in the set of all worlds that are compatible with the knowledge of agent i in any of these worlds.

It should be clear that: whenever two worlds are in the same equivalence class for agent i, i.e., reachable via edges of the same type $R_i$ then $K_iF$, for any F, must either holds in both worlds or none of them.

Now, we can see how this model can be used to represent agents' knowledge with a small example:

Agent 1 knows nothing about the current weather in Manaus. Let m be the proposition "It's raining in Manaus". The knowledge of agent 1 can be written as: $\neg K_1m\land\neg K_1\neg m$, and by diagram:

Attach:Minh/Uploads/ML-1-knows-nothing-Manaus-diagram.png Δ

What is the intuitive meaning of this diagram? Well, worlds $w_1$ and $w_2$ are in the same equivalence class of agent 1. But m holds in $w_1$ and $\neg m$ holds in $w_2$, hence agent 1 cannot distinguish between m and $\neg m$. In other words, agent 1 doesn't know whether it's raining in Manaus or not.

Now, if agent 2 knows that it's raining in Manaus, can we represent agent 1 and 2's knowledge as follows:

Attach:Minh/Uploads/ML-1-knows-nothing-Manaus-2-knows-diagram.jpg Δ

Here comes the confusion. If we only have agent 2 then we also need $w_1$ with m holds inside. But because we need to represent agent 1's knowledge, we must have $w_2$. And the diagram above can only represent that agent 2 knows whether it's raining in Manaus. The appropriate modal formula for agent 2's knowledge is: $K_2m\lor K_2m$

What can be the solution for this situation? Well, simply we just need to explicitly point out which is the actual world for agent 2. When the actual world for agent 2 is $w_1$, she knows that it's raining in Manaus; and when her actual world is $w_2$, she knows that it's not raining in Manaus.

Let's improve this example a little bit more complex. Let l denote the addition proposition: "It's raining in London", and assume that agent 1 knows that it's raining in London, but agent 2 doesn't. The diagram will be drawn as follows:

Attach:Minh/Uploads/ML-1-2-knows-Manaus-London-diagram.jpg Δ

Again, we need to explicitly point out that $w_1$ and $w_2$ are actual worlds. Let's try it on your own to represent and additional agent 3 who knows nothing about the weather in Manaus and London.

Acknowledgment: This entry was inspired by a lecture in the course Non-classical Logics given by Prof. Chris Fermüller.