nLab S5(m) modal logic

Contents

Contents

Idea

This entry is meant to be about the flavor of modal logic known as S5 modal logic with several (mm \in \mathbb{N}) modal operators and their duals.

The axioms B iB_i

The axiom denoted B iB_i, (see Kracht 1999 for indication of possible reasons) is

  • pK iM ipp \to K_i M_i p.

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

  • ¬K ipK i¬K ip\neg K_i p \to K_i \neg K_i p

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)}

  • S5S5 - this logic is obtained from S4S4 by adding the axiom BB.

  • S5 (m)S5_{(m)} starting from S4 (m)S4_{(m)} the logic S4(m), add, for each i=1,,mi = 1,\ldots, m the axiom B iB_i.

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

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 Kripke 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.

Proof

(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.

References

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

  • Patrick Blackburn, M. de Rijke and Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001.

  • Marcus Kracht, Tools and Techniques in Modal Logic, Studies in Logic and the Foundation of Mathematics, 142, Elsevier, 1999.

Application to artificial intelligence:

  • J.- J. Ch. Meyer and W. Van der Hoek, Epistemic logic for AI and Computer Science, Cambridge Tracts in Theoretical Computer Science, vol. 41, 1995.

Last revised on July 16, 2023 at 09:22:43. See the history of this page for a list of all contributions to it.