(T modal logic)
Often one considers adding one more axiom:
In some applications especially in Artificial Intelligence, is interpreted as representing a statement that some (fixed) ‘agent’ knows the proposition . It is then a short step to handling the idea of knowledge in a multiagent system where there may be different ‘agents’. In that setting, interprets as ‘agent knows that ’. This leads to modelling of the passage of the interchange of information between neighbours, e.g. we might have three agents and the proposition that ‘agent 2 knows that agent 3 does not know ’.
The basic epistemic logics, and , do not reflect much of our intuition of ‘knowledge’. The -axiom merely says that, if an agent knows and also that agent knows , then the agent knows . There are a series of additional axioms proposed as being appropriate for knowledge, (although, it seems, each has their supporters and detractors!) These are called , , and (and please don’t ask why, … each has its own history).
This is found in two equivalent forms
The first interprets as if is true, then agent considers it possible and the second as atomic statements known by agent are true .
These logics are generated by (resp. ) and the axiom , (resp. axioms for each .
First looking in the monomodal case, suppose that we have a frame then
if and only if .
So the frames that support models for the logic are exactly the reflexive frames.
Suppose is a reflexive frame and take an arbitrary valuation on and a state in so that . We use the first form of above, and have to prove that holds at , i.e., that holds at some state ‘accessible’ from , but as is reflexive, is accessible from itself, … .
For the converse, we will suppose is not reflexive, so there is some state, which is not -related to itself. We will falsify the formula if we can find a valuation and a state such that holds at but does not. (Recall the semantics of : if and only if, for some such that , .)
We need a state with this property and we only know about one namely , so that is the obvious to try! We need a valuation such that 1) and 2) . If we set this works since is not related to itself. (Other values of are irrelevant.) If has no -successors, then we are finished since clearly in that case, , so suppose that is any -successor of , i.e., , then , so , hence as required.