nLab Kripke frame


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



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 states or points)

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

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

But note that, as there are many flavors of modal logic (epistemic, aletheic, deontic, temporal, dynamic, et cetera), there are many different interpretations of the accessibility relation in the corresponding Kripke frame.

Hence a Kripke frame is a concept with an attitude, namely the attitude 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.)


A (uni-modal) Kripke frame is a set WW and a binary RR relation on WW. A multimodal Kripke frame for modal operators { i} iI\{\Box_i\}_{i \in I} is a set WW together with a binary relations R iR_i for each iIi \in I. Equivalently, a uni-modal Kripke frame is a set WW and a coalgebra for the powerset endofunctor, f R:W𝒫(W)f_R: W \to \mathscr{P}(W). A multimodal Kripke frame is, equivalently, a set XX and a coalgebra for the endofunctor 𝒫(I×)\mathscr{P}(I \times -).

A morphism of Kripke frames, called a bounded morphism or p-morphism (short for pseudo-epimorphism) is a homomorphism of the coalgebras.

We call the category of unimodal Kripke frames Kr\mathbf{Kr}. Kr\mathbf{Kr} is dually equivalent to the category of complete, atomic, completely additive boolean algebras with operators. This is the analogue of the result that Set\mathbf{Set} is dually equivalent to the category of complete, atomic boolean algebras.

A Kripke model for a propositional language LL is a Kripke frame W,f R\langle{W, f_R\rangle} together with a valuation V:L𝟚 WV: L \to \mathbb{2}^W which preserves the appropriate logical structure. The non-modal connectives are handled in the usual way with their set-theoretic analogues (intersection for land\land, union for lor\lor, complement for negation, et cetera). For the modal operator \Box, the truth clause is V(p)(w)=1V(\Box p)(w) = 1 if and only if f R(w)V(p)f_R(w) \subseteq V(p).

We often consider particular classes of Kripke frames, identified by common features of the accessibility relations: e.g. reflexivity, transitivity, symmetry Euclidean, density, et cetera. These correspond to the validity of certain logical principles, and so, different modal logics. However, Kripke frames are not sufficient to classify all (normal) modal logics as detailed in Holliday and Litak, 2019. Although every class of Kripke frames defines a normal modal logic for which the class is complete, some normal modal logics are not complete for any class of Kripke frames, a phenomenon known as “Kripke incompleteness.” By duality, this means there are normal modal logics which are not complete with respect to any class of complete, atomic, completely additive boolean algebras with operators .

Below we detail some classes of Kripke frames.

Some classes of Kripke frames

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


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)


The original articles:

Modern exposition

Textbook accounts;

Generalization of Kripke frames:

On Kripke-frame incompleteness:

  • Holliday, W., Litak, T. (2019). Complete Additivity and Modal Incompleteness. The Review of Symbolic Logic, 12(3), 487-535. [doi:10.1017/S1755020317000259]

Last revised on October 25, 2023 at 23:55:45. See the history of this page for a list of all contributions to it.