the logic S5(m)

The epistemic logics S5S5 and S5 (m)S5_{(m)}


(Note that S5=S5 (1)S5 = S5_{(1)}. See S5 modal logic)

Although better than KK (resp. K(m)K(m)), and TT (resp. T(m)T(m)), S4S4 (resp. S4(m)S4(m)) is still not considered adequate for knowledge representation. Because of this further axioms have been put forward, too many to be mentioned here. We will limit ourselves, (at this stage in the development of these entries, at least) to introducing one more axiom, that is a bit more contentious, (but is nice from the nPOV.)

The axioms B iB_i

The axiom denoted B iB_i, (and again refer to Kracht for some indication of possible reasons) is

The interpretation is the ‘if pp is true then agent ii knows that it is possible that pp is true.’

Another axiom that is relevant here is:

The axioms (5) i(5)_i

Axiom (5) interprets as saying ‘If agent ii does not know that pp holds, then (s)he knows that (s)he does not know’. This is termed ‘negative introspection’.

The logics S5S5 and S5 (m)S5_{(m)}

In either case the same result can be obtained by adding in 55 or (5) i(5)_i in place of the corresponding BB.


This is highly doubtful as a property of knowledge when applied to human beings. If an agent is ignorant of the truth of an assertion, it is very often unlikely that (s)he knows this ignorance.

Tim Porter It would be good to have some discussion on this axiom. (Donald Rumsfeld’s known unknowns has been worked to death, (although sometimes quite well done as here), so please… something worth saying :-)). This might stray over to a new entry as I would hope to see what there is to say especially looking to models of ‘why’ an agent ‘knows’ something. My query is whether that aspect has been explored and if so where. My feeling is that in S5 (and elsewhere) the reasons may give a groupoid-like structure (see below about the Kripke semantics) for the geometric semantics.

Equivalence frames

With T (m)T_{(m)}, the models corresponded to frames where each relation R iR_i was reflexive. With S4 (m)S4_{(m)}, the frames needed to be transitive as well. Here we consider the class 𝒮5(m)\mathcal{S}5(m) of models with frames, where each R iR_i is an equivalence relation. These are sometimes called equivalence frames.

Theorem (Soundness of S5 (m)S5_{(m)})

S5 (m)ϕ𝒮5(m)ϕ.S5_{(m)}\vdash \phi \Rightarrow \mathcal{S}5(m)\models \phi.


(We show this for m=1m = 1.) We have already shown (here in the logic S4(m)) that the older axioms TT and (4)(4) hold so it remains to show if we have a frame, 𝔐=((W,R),V)\mathfrak{M}= ((W,R),V), where RR is an equivalence relation on WW then 𝔐B\mathfrak{M}\models B.

We suppose the we have a state ww so that 𝔚,wp\mathfrak{W},w \models p. Now we need to find out if 𝔚,wKMp\mathfrak{W},w \models K M p, so we note that

  1. 𝔚,wKMp\mathfrak{W},w \models K M p if and only if u\forall u with RwuR w u, $𝔚,uMp\mathfrak{W},u \models M p, but

  2. that holds if u\forall u with RwuR w u, there is some vv with RuvR u v and 𝔚,vp\mathfrak{W},v \models p.

However whatever uu we have with RwuR w u, we have RuwR u w as RR is symmetric, and we know, by assumption, that 𝔚,wp\mathfrak{W},w \models p, so we have what we need.


More on S5S5, S5 (m)S5_{(m)} and their applications in Artificial Intelligence can be found in

General books on modal logics which treat these logics thoroughly in the general context include e

[[!redirects the logic S5(m)]] [[!redirects S5(m)]]