Kripke semantics

A Kripke frame or modal frame is a pair ${\displaystyle \langle W,R\rangle }$, where W is a (possibly empty) set, and R is a binary relation on W. Elements of W are called nodes or worlds, and R is known as the accessibility relation.[2]

A Kripke model is a triple ${\displaystyle \langle W,R,\Vdash \rangle }$, where ${\displaystyle \langle W,R\rangle }$ is a Kripke frame, and ${\displaystyle \Vdash }$ is a relation between nodes of W and modal formulas, such that for all w ∈ W and modal formulas A and B:

• ${\displaystyle w\Vdash \neg A}$ if and only if ${\displaystyle w\nVdash A}$,
• ${\displaystyle w\Vdash A\to B}$ if and only if ${\displaystyle w\nVdash A}$ or ${\displaystyle w\Vdash B}$,
• ${\displaystyle w\Vdash \Box A}$ if and only if ${\displaystyle u\Vdash A}$ for all ${\displaystyle u}$ such that ${\displaystyle w\;R\;u}$.

We read ${\displaystyle w\Vdash A}$ as “w satisfies A”, “A is satisfied in w”, or “w forces A”. The relation ${\displaystyle \Vdash }$ is called the satisfaction relation, evaluation, or forcing relation. The satisfaction relation is uniquely determined by its value on propositional variables.

A formula A is valid in:

• a model ${\displaystyle \langle W,R,\Vdash \rangle }$, if ${\displaystyle w\Vdash A}$ for all w ∈ W,
• a frame ${\displaystyle \langle W,R\rangle }$, if it is valid in ${\displaystyle \langle W,R,\Vdash \rangle }$ for all possible choices of ${\displaystyle \Vdash }$,
• a class C of frames or models, if it is valid in every member of C.

We define Thm(C) to be the set of all formulas that are valid in C. Conversely, if X is a set of formulas, let Mod(X) be the class of all frames which validate every formula from X.

A modal logic (i.e., a set of formulas) L is sound with respect to a class of frames C, if L ⊆ Thm(C). L is complete wrt C if L ⊇ Thm(C).

Semantics is useful for investigating a logic (i.e. a derivation system) only if the semantic consequence relation reflects its syntactical counterpart, the syntactic consequence relation (derivability).[3] It is vital to know which modal logics are sound and complete with respect to a class of Kripke frames, and to determine also which class that is.

For any class C of Kripke frames, Thm(C) is a normal modal logic (in particular, theorems of the minimal normal modal logic, K, are valid in every Kripke model). However, the converse does not hold in general: while most of the modal systems studied are complete of classes of frames described by simple conditions, Kripke incomplete normal modal logics do exist. A natural example of such a system is Japaridze's Polymodal Logic.

A normal modal logic L corresponds to a class of frames C, if C = Mod(L). In other words, C is the largest class of frames such that L is sound wrt C. It follows that L is Kripke complete if and only if it is complete of its corresponding class.

Consider the schema T : ${\displaystyle \Box A\to A}$. T is valid in any reflexive frame ${\displaystyle \langle W,R\rangle }$: if ${\displaystyle w\Vdash \Box A}$, then ${\displaystyle w\Vdash A}$ since w R w. On the other hand, a frame which validates T has to be reflexive: fix w ∈ W, and define satisfaction of a propositional variable p as follows: ${\displaystyle u\Vdash p}$ if and only if w R u. Then ${\displaystyle w\Vdash \Box p}$, thus ${\displaystyle w\Vdash p}$ by T, which means w R w using the definition of ${\displaystyle \Vdash }$. T corresponds to the class of reflexive Kripke frames.

It is often much easier to characterize the corresponding class of L than to prove its completeness, thus correspondence serves as a guide to completeness proofs. Correspondence is also used to show incompleteness of modal logics: suppose L₁ ⊆ L₂ are normal modal logics that correspond to the same class of frames, but L₁ does not prove all theorems of L₂. Then L₁ is Kripke incomplete. For example, the schema ${\displaystyle \Box (A\leftrightarrow \Box A)\to \Box A}$ generates an incomplete logic, as it corresponds to the same class of frames as GL (viz. transitive and converse well-founded frames), but does not prove the GL-tautology ${\displaystyle \Box A\to \Box \Box A}$.

The following table lists common modal axioms together with their corresponding classes. The naming of the axioms often varies.

Name	Axiom	Frame condition
K	${\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}$	N/A
T	${\displaystyle \Box A\to A}$	reflexive: ${\displaystyle w\,R\,w}$
4	${\displaystyle \Box A\to \Box \Box A}$	transitive: ${\displaystyle w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u}$
	${\displaystyle \Box \Box A\to \Box A}$	dense: ${\displaystyle w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)}$
D	${\displaystyle \Box A\to \Diamond A}$ or ${\displaystyle \Diamond \top }$	serial: ${\displaystyle \forall w\,\exists v\,(w\,R\,v)}$
B	${\displaystyle A\to \Box \Diamond A}$	symmetric : ${\displaystyle w\,R\,v\Rightarrow v\,R\,w}$
5	${\displaystyle \Diamond A\to \Box \Diamond A}$	Euclidean: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v}$
GL	${\displaystyle \Box (\Box A\to A)\to \Box A}$	R transitive, R−1 well-founded
Grza	${\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}$	R reflexive and transitive, R−1−Id well-founded
H	${\displaystyle \Box (\Box A\to B)\lor \Box (\Box B\to A)}$	${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u}$
M	${\displaystyle \Box \Diamond A\to \Diamond \Box A}$	(a complicated second-order property)
G	${\displaystyle \Diamond \Box A\to \Box \Diamond A}$	convergent: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)}$
	${\displaystyle A\to \Box A}$	discrete: ${\displaystyle w\,R\,v\Rightarrow w=v}$
	${\displaystyle \Diamond A\to \Box A}$	partial function: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u=v}$
	${\displaystyle \Diamond A\leftrightarrow \Box A}$	function: ${\displaystyle \forall w\,\exists !u\,w\,R\,u}$
	${\displaystyle \Box A}$ or ${\displaystyle \Box \bot }$	empty: ${\displaystyle \forall w\,\forall u\,\neg (w\,R\,u)}$

The following table lists several common normal modal systems. Frame conditions for some of the systems were simplified: the logics are complete with respect to the frame classes given in the table, but they may correspond to a larger class of frames.

Name	Axioms	Frame condition
K	—	all frames
T	T	reflexive
K4	4	transitive
S4	T, 4	preorder
S5	T, 5 or D, B, 4	equivalence relation
S4.3	T, 4, H	total preorder
S4.1	T, 4, M	preorder, ${\displaystyle \forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))}$
S4.2	T, 4, G	directed preorder
GL, K4W	GL or 4, GL	finite strict partial order
Grz, S4Grz	Grz or T, 4, Grz	finite partial order
D	D	serial
D45	D, 4, 5	transitive, serial, and Euclidean

For any normal modal logic, L, a Kripke model (called the canonical model) can be constructed that refutes precisely the non-theorems of L, by an adaptation of the standard technique of using maximal consistent sets as models. Canonical Kripke models play a role similar to the Lindenbaum–Tarski algebra construction in algebraic semantics.

A set of formulas is L-consistent if no contradiction can be derived from it using the theorems of L, and Modus Ponens. A maximal L-consistent set (an L-MCS for short) is an L-consistent set that has no proper L-consistent superset.

The canonical model of L is a Kripke model ${\displaystyle \langle W,R,\Vdash \rangle }$, where W is the set of all L-MCS, and the relations R and ${\displaystyle \Vdash }$ are as follows:

${\displaystyle X\;R\;Y}$ if and only if for every formula ${\displaystyle A}$, if ${\displaystyle \Box A\in X}$ then ${\displaystyle A\in Y}$,

${\displaystyle X\Vdash A}$ if and only if ${\displaystyle A\in X}$.

The canonical model is a model of L, as every L-MCS contains all theorems of L. By Zorn's lemma, each L-consistent set is contained in an L-MCS, in particular every formula unprovable in L has a counterexample in the canonical model.

The main application of canonical models are completeness proofs. Properties of the canonical model of K immediately imply completeness of K with respect to the class of all Kripke frames. This argument does not work for arbitrary L, because there is no guarantee that the underlying frame of the canonical model satisfies the frame conditions of L.

We say that a formula or a set X of formulas is canonical with respect to a property P of Kripke frames, if

• X is valid in every frame that satisfies P,
• for any normal modal logic L that contains X, the underlying frame of the canonical model of L satisfies P.

A union of canonical sets of formulas is itself canonical. It follows from the preceding discussion that any logic axiomatized by a canonical set of formulas is Kripke complete, and compact.

The axioms T, 4, D, B, 5, H, G (and thus any combination of them) are canonical. GL and Grz are not canonical, because they are not compact. The axiom M by itself is not canonical (Goldblatt, 1991), but the combined logic S4.1 (in fact, even K4.1) is canonical.

In general, it is undecidable whether a given axiom is canonical. We know a nice sufficient condition: Henrik Sahlqvist identified a broad class of formulas (now called Sahlqvist formulas) such that

• a Sahlqvist formula is canonical,
• the class of frames corresponding to a Sahlqvist formula is first-order definable,
• there is an algorithm that computes the corresponding frame condition to a given Sahlqvist formula.

This is a powerful criterion: for example, all axioms listed above as canonical are (equivalent to) Sahlqvist formulas.

A logic has the finite model property (FMP) if it is complete with respect to a class of finite frames. An application of this notion is the decidability question: it follows from Post's theorem that a recursively axiomatized modal logic L which has FMP is decidable, provided it is decidable whether a given finite frame is a model of L. In particular, every finitely axiomatizable logic with FMP is decidable.

There are various methods for establishing FMP for a given logic. Refinements and extensions of the canonical model construction often work, using tools such as filtration or unravelling. As another possibility, completeness proofs based on cut-free sequent calculi usually produce finite models directly.

Most of the modal systems used in practice (including all listed above) have FMP.

In some cases, we can use FMP to prove Kripke completeness of a logic: every normal modal logic is complete with respect to a class of modal algebras, and a finite modal algebra can be transformed into a Kripke frame. As an example, Robert Bull proved using this method that every normal extension of S4.3 has FMP, and is Kripke complete.

Kripke semantics has a straightforward generalization to logics with more than one modality. A Kripke frame for a language with ${\displaystyle \{\Box _{i}\mid \,i\in I\}}$ as the set of its necessity operators consists of a non-empty set W equipped with binary relations R_i for each i ∈ I. The definition of a satisfaction relation is modified as follows:

${\displaystyle w\Vdash \Box _{i}A}$ if and only if ${\displaystyle \forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).}$

A simplified semantics, discovered by Tim Carlson, is often used for polymodal provability logics. A Carlson model is a structure ${\displaystyle \langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle }$ with a single accessibility relation R, and subsets D_i ⊆ W for each modality. Satisfaction is defined as

${\displaystyle w\Vdash \Box _{i}A}$ if and only if ${\displaystyle \forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).}$

Carlson models are easier to visualize and to work with than usual polymodal Kripke models; there are, however, Kripke complete polymodal logics which are Carlson incomplete.

Let L be a first-order language. A Kripke model of L is a triple ${\displaystyle \langle W,\leq ,\{M_{w}\}_{w\in W}\rangle }$, where ${\displaystyle \langle W,\leq \rangle }$ is an intuitionistic Kripke frame, M_w is a (classical) L-structure for each node w ∈ W, and the following compatibility conditions hold whenever u ≤ v:

• the domain of M_u is included in the domain of M_v,
• realizations of function symbols in M_u and M_v agree on elements of M_u,
• for each n-ary predicate P and elements a₁,...,a_n ∈ M_u: if P(a₁,...,a_n) holds in M_u, then it holds in M_v.

Given an evaluation e of variables by elements of M_w, we define the satisfaction relation ${\displaystyle w\Vdash A[e]}$:

• ${\displaystyle w\Vdash P(t_{1},\dots ,t_{n})[e]}$ if and only if ${\displaystyle P(t_{1}[e],\dots ,t_{n}[e])}$ holds in M_w,
• ${\displaystyle w\Vdash (A\land B)[e]}$ if and only if ${\displaystyle w\Vdash A[e]}$ and ${\displaystyle w\Vdash B[e]}$,
• ${\displaystyle w\Vdash (A\lor B)[e]}$ if and only if ${\displaystyle w\Vdash A[e]}$ or ${\displaystyle w\Vdash B[e]}$,
• ${\displaystyle w\Vdash (A\to B)[e]}$ if and only if for all ${\displaystyle u\geq w}$, ${\displaystyle u\Vdash A[e]}$ implies ${\displaystyle u\Vdash B[e]}$,
• not ${\displaystyle w\Vdash \bot [e]}$,
• ${\displaystyle w\Vdash (\exists x\,A)[e]}$ if and only if there exists an ${\displaystyle a\in M_{w}}$ such that ${\displaystyle w\Vdash A[e(x\to a)]}$,
• ${\displaystyle w\Vdash (\forall x\,A)[e]}$ if and only if for every ${\displaystyle u\geq w}$ and every ${\displaystyle a\in M_{u}}$ , ${\displaystyle u\Vdash A[e(x\to a)]}$.

Here e(x→a) is the evaluation which gives x the value a, and otherwise agrees with e.

See a slightly different formalization in.[4]

As part of the independent development of sheaf theory, it was realised around 1965 that Kripke semantics was intimately related to the treatment of existential quantification in topos theory.[5] That is, the 'local' aspect of existence for sections of a sheaf was a kind of logic of the 'possible'. Though this development was the work of a number of people, the name Kripke–Joyal semantics is often used in this connection.