nLab
geometric model for modal logics

Contents

Models in Modal Logics

To give the standard (geometric) semantics of modal logics, one needs models and these will be discussed here and in the companion algebraic models for modal logics.

(This outlines the basics of the semantics often called Kripke semantics of these logics. We concentrate on modal languages with unary modalities and therefore on relational structures with binary relations in them only. This is largely for the sake of keeping the exposition fairly straightforward and simple. This means the frames used will be β€˜Kripke frames’. There may be a need later (or elsewhere in the Lab) to discuss more general frames.)

Models in Monomodal Logics

Again we look at the basic model language.

Definition

A model for β„’ Ο‰(1)\mathcal{L}_\omega(1) is a pair 𝔐=(𝔉,V)\mathfrak{M} = (\mathfrak{F},V), where 𝔉\mathfrak{F} is a frame (for β„’ Ο‰(1)\mathcal{L}_\omega(1)) and V:Prop→𝒫(W)V: Prop \to \mathcal{P}(W), is a function, called a valuation, assigning to each atomic proposition pp a subset of the set, WW, of worlds.

Gloss

  1. Informally we think of V(p)V(p) as the set of β€˜worlds’ in our model where pp is true.

  2. Frames are β€˜mathematical pictures’ of ontologies that are found interesting (for the context), whilst a model β€˜puts some flesh on’ the frame by adding contingent information.

  3. Frames give a combinatorial, relational or geometric basis for the semantics of these logics. There is also an algebraic semantics that will be examined in another entry. (To be done)

Satisfaction

Definition

Suppose that ww is a state in a model 𝔐=(W,R,V)\mathfrak{M} = (W,R,V). We inductively define the notion of a formula Ο•\phi being satisfied in the model at state ww, as follows:

  • for p∈Propp\in Prop, 𝔐,w⊧p\mathfrak{M},w \models p if and only if w∈V(p)w\in V(p);

  • 𝔐,w⊧βŠ₯\mathfrak{M},w \models \bot never;

  • 𝔐,wβŠ§Β¬Ο•\mathfrak{M},w \models \neg \phi if and only if it is not true that 𝔐,wβŠ§Ο•\mathfrak{M},w \models \phi;

  • 𝔐,wβŠ§Ο•βˆ¨Οˆ\mathfrak{M},w \models \phi \vee \psi if and only if 𝔐,wβŠ§Ο•\mathfrak{M},w \models\phi or 𝔐,w⊧ψ\mathfrak{M},w \models\psi;

  • 𝔐,wβŠ§β‹„Ο•\mathfrak{M},w \models \Diamond \phi if and only if, for some v∈Wv \in W such that Rwv R w v, 𝔐,vβŠ§Ο•\mathfrak{M},v \models \phi.

Notes

  1. The terminology used in talking about β€˜satisfaction’ tends to interpret 𝔐,vβŠ§Ο•\mathfrak{M},v \models \phi as saying the formula Ο•\phi is true in 𝔐\mathfrak{M} at state vv. We will adopt this usage, but we will avoid entering into the niceties of discussing β€˜what is truth?’,… at least in this entry!

  2. 𝔐,wβŠ§β–‘Ο•\mathfrak{M},w \models \square \phi if and only if βˆ€v∈W\forall v\in W Rwn R w n implies 𝔐,vβŠ§Ο•\mathfrak{M},v \models \phi. (The proof is fairly routine manipulation of negations.)

  3. We say a set Ξ£\Sigma of formulae is true at state w∈Ww\in W of a model 𝔐\mathfrak{M}, written 𝔐,w⊧Σ\mathfrak{M},w \models \Sigma, if all members of Ξ£\Sigma are satisfied as ww.

  4. It is convenient to extend the valuation VV to arbitrary formulae by setting V(Ο•):={wβˆ£π”,wβŠ§Ο•}V(\phi) := \{w \mid \mathfrak{M},w \models \phi\}. We then get useful interpretations such as: if for all worlds vv, 𝔐,v⊧(Ο•β†’Οˆ)\mathfrak{M},v \models (\phi\to \psi) and modus ponens holds, (i.e. we have a logic as such in which we are working, then V(Ο•)βŠ†V(ψ)V(\phi)\subseteq V(\psi). (This comment is deliberately slightly vague, but indicates a common type of argument that will be behind many results, where more precision is available, so think of it as a template for a result rather than a result as such.)

What is a valuation?

In the definition of a Kripke model the valuation is all important. It is what puts meaning onto the frame. It is very useful to push this idea around through a couple of adjunctions and reinterpretations. The process is fairly intuitive, but it pays to do things reasonably formally:

  1. Note that the power set 𝒫(W)\mathcal{P}(W) can also be written as 2 W\mathbf{2}^W the set of functions from WW to 2\mathbf{2}, where we write 2\mathbf{2} for the β€˜set’ of classical truth values, {βŠ₯β†’βŠ€}\{\bot \to \top\}, or {true,false}\{true,false\}, or {0,1}\{0,1\} or … . We wrote β€˜set’ in inverted commas for several reasons:

    • Firstly an important role here is played by the multiple structures that 2\mathbf{2} has. It is a Heyting algebra; it has a natural poset structure; it is the subobject classifier in the topos of sets, and so on. In fact it is the source of most of the logic semantic structure within this context. Its structure induces similar structures on the powerset, 𝒫(W)\mathcal{P}(W), given by union etc, that made the semantics work above. (See also the discussion on ambimorphic objects in the entry on the Chu construction.)

    • Next note that although we said β€˜set’ we could do a lot of this in other settings. For instance we could work within a more general topos with an object of possible worlds and an object of propositions. We would need the extra Heyting algebra structure on what would there probably be written as Ξ©\Omega, and our negation interpretation would be more subtle.

    • Finally we could categorify things. For the moment we will leave this aside, but note the discussion at truth value.

  2. For convenience we will write PP for PropProp, then a valuation is V:Pβ†’2 WV: P\to \mathbf{2}^W, and using cocurrying this corresponds to V:PΓ—Wβ†’2V: P\times W\to \mathbf{2}. That, of course, corresponds to a subset of PΓ—WP\times W. That subset consists of all pairs, (p,w)(p,w), for which w∈V(p)w\in V(p) so interprets as the set of pairs in which the proposition pp is β€˜true’ in world ww.

  3. We could recurry after transposing PP and WW, to get VV to correspond to V˜:W→𝒫(P)\tilde{V}: W \to \mathcal{P}(P), so that V˜(w)\tilde{V}(w) is the set of propositions true about the world ww.

  4. Another useful direction is to see this as giving a binary Chu space. (To be investigated later.)

Models in Multimodal Logics

Again we look at the basic model language this time with nn unary modal operators.

Definition

A model for β„’ Ο‰(n)\mathcal{L}_\omega(n) is a pair 𝔐=(𝔉,V)\mathfrak{M} = (\mathfrak{F},V), where 𝔉\mathfrak{F} is a frame (for β„’ Ο‰(n)\mathcal{L}_\omega(n)) and V:Prop→𝒫(W)V: Prop \to \mathcal{P}(W), is a function, called a valuation, assigning to each atomic proposition pp a subset of the set, WW, of worlds.

Satisfaction in the multimodal case

This is virtually the same as in the monomodal case, except for the last case which involves the nn modal operators. (We give it in full repeating the earlier cases for convenience.)

Definition

Suppose that ww is a state in a model 𝔐=(W,R,V)\mathfrak{M} = (W,R,V). We inductively define the notion of a formula Ο•\phi being satisfied in the model at state ww, as follows:

  • for p∈Propp\in Prop, 𝔐,w⊧p\mathfrak{M},w \models p if and only if w∈V(p)w\in V(p);

  • 𝔐,w⊧βŠ₯\mathfrak{M},w \models \bot never;

  • 𝔐,wβŠ§Β¬Ο•\mathfrak{M},w \models \neg \phi if and only if it is not true that 𝔐,wβŠ§Ο•\mathfrak{M},w \models \phi;

  • 𝔐,wβŠ§Ο•βˆ¨Οˆ\mathfrak{M},w \models \phi \vee \psi if and only if 𝔐,wβŠ§Ο•\mathfrak{M},w \models\phi or 𝔐,w⊧ψ\mathfrak{M},w \models\psi;

  • for each i=1,…,ni = 1, \ldots, n, 𝔐,wβŠ§β‹„ iΟ•\mathfrak{M},w \models \Diamond_i \phi if and only if, for some v∈Wv \in W such that R iwv R_i w v, 𝔐,vβŠ§Ο•\mathfrak{M},v \models \phi.

Satisfaction on a class of models is related to validity of modal formulae. In this way a class of frames can determine a logic and then the logic determines a class of frames. The axiomatisation of that class/logic is then an interesting challenge.

References

Generally this entry is based on

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

(any mistakes or errors of interpretation are due to ….!)

Revised on October 24, 2012 11:57:18 by Urs Schreiber (82.169.65.155)