nLab Kripke frame

Contents

This entry is about models of modal logic; for frames in the sense of geometric logic see instead there.


Contents

Idea

In formal logic, Kripke frames, after Kripke (1959), (1963), serve as the contextual substrate of set-theoretic semantics/models for modal logics (called geometric models as opposed to algebraic models).

In itself, a Kripke frame is just

  • an inhabited set WW

    often called the set of possible worlds (or the set of nodes or whatnot)

  • equipped with an indexed set of binary relations R iW×WPropR_i W \times W \to Prop, one for each modal operator i\Box_i in the given modal logic

    called the accessiblity or transition relations between worlds, or similar, where R i(w,w)R_i (w,w') is interpreted as: “To agent ii in world ww, world ww' appears (just as well) possible.”

Hence a Kripke frame is a concept with an attitude, namely the attidute to serve as a model for a modal logic – the idea is to interpret:

  1. the elements of WW as the “possible worlds” about which the propositions in the modal logic make statements,

  2. the relation R i(w,w)R_i(w,w') as asserting that it makes sense to reason about world ww' at world ww.

Namely a model of the modal logic based on such a Kripke frame will interpret

  • each proposition PP of the logic as a WW-dependent proposition P:WPropP \colon W \to Prop,

  • each modal proposition iP\Box_i P as the WW-dependent proposition which at wWw \in W asserts that “PP holds at all those ww' that are in iith relation to WW”, hence “PP holds in all worlds ww' that ii deems to be just as possible as ww”; formally (eg. Blackburn & van Benthem (2007) p. 10):

(Here we are writing — following notation for subtypesP:WPropP \,\colon\,W \to Prop for a WW-dependent proposition, equivalently a proposition about the elements of WW, equivalently the subset of WW where the proposition holds.)

The transparent case of S5 logic. Specifically, for the case of S5 modal logic with a single comonadic modal operator \Box, a Kripke frame (originally considered in Kripke 1963) is an

equipped with a single

which means that WW decomposes as the disjoint union of its equivalence classes, these being the fibers of the quotient coprojection

(1)Wp WW/R. W \xrightarrow{\;\; p_W \;\;} W/R \,.

The simple case necessity logic. In the further special case there is just a single such class (hence that “all possible worlds are related”, originally considered by Kripke 1959) this becomes

(2)Wp W* W \xrightarrow{\;\; p_W \;\;} \ast

so that in models based on such a frame the interpretation of the modal operator \Box is that of necessity: P\Box P now asserts, independently of the world that it is evaluated on, that PP holds at all wWw \in W, hence that PP holds necessarily in the sense of: no matter which world.

The general case of Kripke frames is really just this basic idea with some variations added. For instance the general case (1) of S5 modal logic is just a W/RW/R-indexed disjoint union of this basic situation.

Perspective of dependent type theory. As discussed in detail at Possible worlds via Dependent types, the Kripke model for the modal operator \Box in the case (2) of S5 modal logic with a global accessibility relation is just the base change comonad along the projection (2), and the same argument immediately applies to the general S5-case (1):

(3)

The case of S4 logic. If the relation RR in a Kripke frame is (reflexive and) transitive but not necessarily symmetric, then it still serves to provide models of S4 modal logic (cf. Kripke 1959, §2).

In this case the relation no longer defines a groupoid (“setoid”) as it does for the S5-case, but it defines a (0,1)-category with objects the elements of WW.

As such, to retain the type-theoretic perspective (3) in this case will require some form of directed type theory.


General case

type of modal logicrelation in its Kripke frames
K modal logicany relation
K4 modal logic?transitive relation
T modal logicreflexive relation
B modal logic?symmetric relation
S4 modal logicreflexive & transitive relation
S5 modal logicequivalence relation

(following BdRV (2001) Table 4.1; cf. Fagin, Halpern, Moses & Vardi (1995) Thm. 3.1.5)

References

The original articles:

Modern exposition

Textbook accounts;

Generalization of Kripke frames:

Last revised on August 3, 2023 at 19:06:05. See the history of this page for a list of all contributions to it.