# Kripke models

Structures consisting of a certain set of ordinary models for classical logic, ordered by a certain relation, and serving for the interpretation of various non-classical logics (intuitionistic, modal, etc.). More precisely: A Kripke model for a language $L$ is given by

$$K = ( S, R, D, W),$$

where $S$ is a non-empty set (of "worlds" , "situations" ); $R$ is a binary relation on $S$( for example, for the system $J$ of intuitionistic logic, $R$ is a partial order; for the modal system (cf. Modal logic) $S4$ it is a pre-order; for the system $S5$ it is an equivalence relation); $D$ is a mapping which associates with each $\alpha \in S$ a non-empty domain $D _ \alpha$ such that, if $\alpha R \beta$, then $D _ \alpha \subseteq D _ \beta$; $W$ is a valuation which associates with each individual constant $a$ of the language $L$ an element $W ( a) \in \cap _ {\alpha \in S } D _ \alpha$, and with each individual variable $x$ an element $W ( x) \in \cup _ {\alpha \in S } D _ \alpha$; for each $\alpha \in S$, $W$ associates with each propositional variable $p$ a truth value $W _ \alpha ( p) \in \{ \textrm{ T } , \textrm{ F } \}$( for the system $J$ it is also stipulated that if $\alpha R \beta$ and $W _ \alpha ( p) = \textrm{ T }$, then $W _ \beta ( p) = \textrm{ T }$); with each $n$- placed ( $n \geq 1$) predicate symbol $P$ a certain subset $W _ \alpha ( P) \subseteq ( D _ \alpha ) ^ {n}$( for the system $J$, if $\alpha R \beta$, then $W _ \alpha ( P) \subseteq W _ \beta ( P)$); and with each $n$- placed function symbol $f$ a function $W _ \alpha ( f )$ from $( D _ \alpha ) ^ {n}$ to $D _ \alpha$( for the system $J$, if $\alpha R \beta$, then $W _ \alpha ( f )$ is the restriction of $W _ \beta ( f )$ to $D _ \alpha$).

For any $\alpha \in S$ and any formula $A$ of $L$ such that for each free variable $x$ in $A$ one has $W ( x) \in D _ \alpha$, the truth value $W _ \alpha ( A) \in \{ \textrm{ T } , \textrm{ F } \}$ is defined inductively. For the system $J$, $W _ \alpha ( A)$ is defined as follows:

a) if $A$ is an atomic formula, $W _ \alpha ( A)$ is already defined in the model;

b) $W _ \alpha ( B \& C) = \textrm{ T } \leftrightharpoons ( W _ \alpha ( B) = \textrm{ T } \textrm{ and } W _ \alpha ( C) = \textrm{ T } )$;

c) $W _ \alpha ( B \lor C) = \textrm{ T } \leftrightharpoons ( W _ \alpha ( B) = \textrm{ T } \textrm{ or } W _ \alpha ( C) = \textrm{ T } )$;

d) $W _ \alpha ( B \supset C) = \textrm{ T } \leftrightharpoons$ (for any $\beta \in S$, if $\alpha R \beta$ and $W _ \beta ( B) = \textrm{ T }$, then $W _ \beta ( C) = \textrm{ T }$);

e) $W _ \alpha ( \neg B) = \textrm{ T } \leftrightharpoons$ (for any $\beta \in S$, if $\alpha R \beta$, then $W _ \beta ( B) = \textrm{ F }$);

f) $W _ \alpha ( \forall x B) = \textrm{ T } \leftrightharpoons$ (for any $W ^ \prime = _ {x} W$ and $\beta \in S$, if $\alpha R \beta$ and $W ^ \prime ( x) \in D _ \beta$, then $W _ \beta ^ \prime ( B) = \textrm{ T }$);

g) $W _ \alpha ( \exists x B) = \textrm{ T } \leftrightharpoons$ (there exists a $W ^ \prime = _ {x} W$ such that $W ^ \prime ( x) \in D _ \alpha$ and $W _ \alpha ^ \prime ( B) = \textrm{ T }$)

(here $W ^ \prime = _ {x} W$ means that the valuation $W ^ \prime$ coincides with $W$ everywhere, except possibly on $x$). Instead of $W _ \alpha ( A) = \textrm{ T }$ one sometimes writes $\alpha \vDash A$.

For modal logics, the definition of $W _ \alpha ( A)$ in cases d, e and g is different:

d') $W _ \alpha ( B \supset C) = \textrm{ T } \leftrightharpoons ( W _ \alpha ( B) = \textrm{ F } \textrm{ or } W _ \alpha ( C) = \textrm{ T } )$;

e') $W _ \alpha ( \neg B) = \textrm{ T } \leftrightharpoons W _ \alpha ( B) = \textrm{ F }$;

g') $W _ \alpha ( \forall x B) = \textrm{ T } \leftrightharpoons$( for any $W ^ \prime = _ {x} W$, if $W ^ \prime ( x) \in D _ \alpha$, then $W _ \alpha ^ \prime ( B) = \textrm{ T }$);

h) $W _ \alpha ( \square B) = \textrm{ T } \leftrightharpoons$ (for any $\beta \in S$, if $\alpha R \beta$, then $W _ \beta ( B) = \textrm{ T }$).

A formula $A$ is said to be true in a Kripke model $K = ( S, R, D, W)$( written $K \vDash A$) if $W _ \alpha ( A) = \textrm{ T }$ for any $\alpha \in S$. For each of the systems $J$, $S4$ and $S5$ one has the completeness theorem: A formula is deducible in the system if and only if it is true in all Kripke models of the corresponding class. It is essential that the domains $D _ \alpha$ are in general different, since the formula

$$\tag{* } \forall x ( A \lor B ( x)) \supset A \lor \forall x B ( x),$$

where $x$ is not free in $A$, is not deducible in $J$, but it is true in all Kripke models with constant domain. The system obtained from $J$ by adding the scheme (*) is complete relative to Kripke models with constant domain (see ). The propositional fragment of each of the systems $J$, $S4$ and $S5$ is finitely approximable, i.e. any formula which is not deducible in the system is refutable in some finite Kripke model of the corresponding class.

The concept of a "Kripke model" , due to S.A. Kripke, is related to that of forcing (see Forcing method).

How to Cite This Entry:
Kripke models. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Kripke_models&oldid=51296
This article was adapted from an original article by S.K. Sobolev (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article