nLab Kripke frame

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

---

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 $W$

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

• equipped with an indexed set of binary relations $R_i W \times W \to Prop$, one for each modal operator $\Box_i$ in the given modal logic

  called the accessiblity or transition relations between worlds, or similar, where $R_i (w,w')$ is interpreted as: “To agent $i$ in world $w$, world $w'$ 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 $W$ as the “possible worlds” about which the propositions in the modal logic make statements,

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

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

• each proposition $P$ of the logic as a $W$-dependent proposition $P \colon W \to Prop$,

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

(Here we are writing — following notation for subtypes — $P \,\colon\,W \to Prop$ for a $W$-dependent proposition, equivalently a proposition about the elements of $W$, equivalently the subset of $W$ 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

• inhabited set$\;$ $W$

equipped with a single

• equivalence relation$\;$ $R$

  (hence a relation which is reflexive, transitive and symmetric)

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

(1)$$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)$$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: $\Box P$ now asserts, independently of the world that it is evaluated on, that $P$ holds at all $w \in W$, hence that $P$ 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/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 $R$ 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 $W$.

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 logic	relation in its Kripke frames
K modal logic	any relation
K4 modal logic?	transitive relation
T modal logic	reflexive relation
B modal logic?	symmetric relation
S4 modal logic	reflexive & transitive relation
S5 modal logic	equivalence relation

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

Related entries

• possible worlds

• necessity and possibility

• epistemic modal logic

References

The original articles:

• Saul A. Kripke, A Completeness Theorem in Modal Logic, The Journal of Symbolic Logic 24 1 (1959) 1-14 [doi:10.2307/2964568, jstor:2964568, pdf]

• Saul A. Kripke, Semantical Analysis of Modal Logic I. Normal Modal Propositional Calculi, Mathematical Logic Quaterly 9 5-6 (1963) 67-96 [doi:10.1002/malq.19630090502]

• Saul A. Kripke, Semantical Considerations on Modal Logic, Acta Philosophical Fennica 16 (1963) 83-94 [pdf]

• Saul A. Kripke, Semantical Analysis of Modal Logic II. Non-Normal Modal Propositional Calculi, in The Theory of Models (Proceedings of the 1963 International Symposium at Berkeley) Studies in Logic and the Foundations of Mathematics (1965) 206-220 [doi:10.1016/B978-0-7204-2233-7.50026-5]

Modern exposition

• Patrick Blackburn, Johan van Benthem, Modal logic: a semantic perspective, Ch 1 in: The Handbook of Modal Logic, Studies in Logic and Practical Reasoning 3 (2007) [doi:10.1016/S1570-2464(07)80004-8, book webpage]

Textbook accounts;

• Patrick Blackburn, Maarten de Rijke, Yde Venema, §1.3 in: Modal Logic, Cambridge Tracts in Theoretical Computer Science 53, Cambridge University Press (2001) [doi:10.1017/CBO9781107050884]

• Valentin Goranko, Martin Otto, §1.2 in: Model Theory of Modal Logic, in Section 5 in: Handbook of Modal Logic, Studies in Logic and Practical Reasoning 3 (2007) 249-329 [pdf, book webpage, publisher page]

• Olivier Gasquet, Andreas Herzig, Bilal Said, François Schwarzentruber, Kripke’s Worlds: An Introduction to Modal Logics via Tableaux, Studies in Universal Logic, Springer (2014) [doi:10.1007/978-3-7643-8504-0, ISBN:978-3764385033]

Generalization of Kripke frames:

• Dov Samet, §6 in: S5 knowledge without partitions, Synthese 172 (2010) 145–155 [doi:10.1007/s11229-009-9469-0]