nLab
the logic T(m)

The epistemic logics TT and T (m)T_{(m)}

Idea

The flavor of modal logic called TT is propositional logic equipped with a single modality usually written ‘’\Box“ subject to the rules that for all propositions p,q:Propp, q \colon Prop we have

  1. K:(pq)(pq)\Box K \colon \Box(p \to q) \to (\Box p \to \Box q) (K modal logic)

  2. T:pp\Box T \colon \Box p \to p (T modal logic)

Often one considers adding one more axiom:

  • 4:pp\Box 4 \colon \Box p \to \Box \Box p. (S4 modal logic).

In some applications especially in Artificial Intelligence, p\Box p is interpreted as representing a statement that some (fixed) ‘agent’ knows the proposition pp. It is then a short step to handling the idea of knowledge in a multiagent system where there may be mm different ‘agents’. In that setting, ip\Box_i p interprets as ‘agent ii knows that pp’. 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 pp’.

The basic epistemic logics, KK and K (m)K_{(m)}, do not reflect much of our intuition of ‘knowledge’. The KK-axiom merely says that, if an agent knows ϕ\phi and also that agent knows ϕψ\phi\to \psi, then the agent knows ψ\psi. 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 TT, (4)(4), and BB (and please don’t ask why, … each has its own history).

The axioms T iT_i

This is found in two equivalent forms

  • pM ipp\to M_i p

and

  • K ippK_i p\to p.

The first interprets as if pp is true, then agent ii considers it possible and the second as atomic statements known by agent ii are true .

The logics TT and T (m)T_{(m)}

These logics are generated by KK (resp. K (m)K_{(m)}) and the axiom TT, (resp. axioms T iT_i for each i=1,mi = 1,\ldots m.

Semantics

First looking in the monomodal case, suppose that we have a frame 𝔉=(W,R)\mathfrak{F} = (W,R) then

Proposition

𝔉T\mathfrak{F}\models T if and only if 𝔉wW,Rww\mathfrak{F} \models \forall w\in W,\; R w w.

So the frames that support models for the logic TT are exactly the reflexive frames.

Proof

Suppose 𝔉\mathfrak{F} is a reflexive frame and take an arbitrary valuation VV on 𝔉\mathfrak{F} and a state ww in 𝔉\mathfrak{F} so that (𝔉,V),wp(\mathfrak{F},V),w\models p. We use the first form of TT above, and have to prove that MpM p holds at ww, i.e., that pp holds at some state ‘accessible’ from ww, but as RR is reflexive, ww is accessible from itself, … .

For the converse, we will suppose RR is not reflexive, so there is some state, wWw \in W which is not RR-related to itself. We will falsify the formula TT if we can find a valuation VV and a state vv such that pp holds at vv but MpM p does not. (Recall the semantics of MM: 𝔐,wMϕ\mathfrak{M},w \models M \phi if and only if, for some vWv \in W such that Rwv R w v, 𝔐,vϕ\mathfrak{M},v \models \phi.)

We need a state with this property and we only know about one namely ww, so that is the obvious to try! We need a valuation such that 1) wV(p)w\in V(p) and 2) {xWRwx}V(p)=\{x\in W\mid R w x\}\cap V(p)= \empty. If we set V(p)={w}V(p) = \{w\} this works since ww is not related to itself. (Other values of VV are irrelevant.) If ww has no RR-successors, then we are finished since clearly in that case, ¬(wMϕ)\neg(w \models M \phi), so suppose that vv is any RR-successor of ww, i.e., RwvR w v, then wvw\neq v, so ¬(vp)\neg(v\models p), hence ¬(wMp)\neg(w\models M p) as required.\blacksquare

Revised on November 6, 2012 00:43:12 by Tim Porter (95.147.237.115)