nLab geometric model for modal logics

Redirected from "Kripke semantics".
Contents

Contents

Models in Modal Logics

The semantics of modal logics based on Kripke frames (“geometric” in contrast to algebraic models for modal logics), often called Kripke semantics [Kripke (1959), (1963)].

In the following we say frame for Kripke frame.

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)), that is, a non-empty set, WW, equipped with a binary relation, RR, 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. The binary relation of the frame allows for the modelling of the truth of a modal proposition, ϕ\Diamond \phi or ϕ\Box \phi, at some world in terms of the truth of ϕ\phi at related worlds.

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 pPropp\in Prop, 𝔐,wp\mathfrak{M},w \models p if and only if wV(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 vWv \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.

  2. 𝔐,wϕ\mathfrak{M},w \models \square \phi if and only if vW\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 wWw\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:P2 WV: P\to \mathbf{2}^W, and using cocurrying this corresponds to V:P×W2V: 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 wV(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 pPropp\in Prop, 𝔐,wp\mathfrak{M},w \models p if and only if wV(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 vWv \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

The concept originates with:

Textbook accounts:

Generalization beyond Kripke frames:

Last revised on July 27, 2023 at 19:31:17. See the history of this page for a list of all contributions to it.