View source for Kripke models

<!--
k0558501.png
$#A+1 = 127 n = 0
$#C+1 = 127 : ~/encyclopedia/old_files/data/K055/K.0505850 Kripke models
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

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|intuitionistic logic]],  $  R $
is a partial order; for the modal system (cf. [[Modal logic|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 }  \rightharpoonup ^  \huL    ( W _  \alpha  ( B) = \textrm{ T }   \textrm{ and }   W _  \alpha  ( C) = \textrm{ T } ) $;

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

d)  $  W _  \alpha  ( B \supset C) = \textrm{ T }  \rightharpoonup ^  \huL   $(
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 }  \rightharpoonup ^  \huL   $(
for any  $  \beta \in S $, 
if  $  \alpha R \beta $, 
then  $  W _  \beta  ( B) = \textrm{ F } $);

f)  $  W _  \alpha  ( \forall x  B) = \textrm{ T }  \rightharpoonup ^  \huL   $(
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 }  \rightharpoonup ^  \huL   $(
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 }  \rightharpoonup ^  \huL    ( W _  \alpha  ( B) = \textrm{ F }   \textrm{ or }   W _  \alpha  ( C) = \textrm{ T } ) $;

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

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

and, in addition, one requires

h)  $  W _  \alpha  ( \square B) = \textrm{ T }  \rightharpoonup ^  \huL   $(
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 [[#References|[3]]]). 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|Forcing method]]).

====References====
<table><TR><TD valign="top">[1a]</TD> <TD valign="top">  S.A. Kripke,   "A completeness theorem in modal logic"  ''J. Symbolic Logic'' , '''24'''  (1959)  pp. 1–14</TD></TR><TR><TD valign="top">[1b]</TD> <TD valign="top">  S.A. Kripke,   "The undecidability of monadic modal quantification theory"  ''Z. Math. Logik Grundl. Math.'' , '''8'''  (1962)  pp. 113–116</TD></TR><TR><TD valign="top">[1c]</TD> <TD valign="top">  S.A. Kripke,   "Semantical analysis of modal logic, I"  ''Z. Math. Logik Grundl. Math.'' , '''9'''  (1963)  pp. 67–96</TD></TR><TR><TD valign="top">[1d]</TD> <TD valign="top">  S.A. Kripke,   "Semantical analysis of modal logic, II"  J.W. Addison (ed.)  L. Henkin (ed.)  A. Tarski (ed.) , ''The theory of models'' , North-Holland  (1965)  pp. 206–220</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  K. Schütte,   "Vollständige Systeme modaler und intuitionistischer Logik" , Springer  (1968)</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  S. Görnemann,   "A logic stronger than intuitionism"  ''J. Symbolic Logic'' , '''36'''  (1971)  pp. 249–261</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  P.J. Cohen,   "Set theory and the continuum hypothesis" , Benjamin  (1966)</TD></TR></table>

====Comments====
Kripke models for intuitionistic logic are a special case of topos-theoretic models (cf. also [[Topos|Topos]]). Specifically, the function  $  D $
in the definition may be regarded as a pre-sheaf (i.e., a set-valued functor) on the partially ordered set  $  ( S, R) $; 
the function  $  W $
equips this pre-sheaf with a structure for the given language, internally in the topos of pre-sheaves on  $  ( S, R) $, 
and the inductive definition of validity, given above, is the external interpretation of internal validity in this topos. Kripke semantics remain sound (cf. also [[Sound rule|Sound rule]]) for models in any topos of pre-sheaves (that is, if the partial order  $  ( S, R) $
is replaced by an arbitrary small category  $  {\mathcal C} $) 
— one has only to replace the quantification over nodes  $  \beta $
such that  $  \alpha R \beta $, 
which occurs in clauses d), e) and f), by a quantification over morphisms of  $  {\mathcal C} $
with domain  $  \alpha $. 
However, if one considers models in a topos of sheaves (that is, if one introduces a Grothendieck topology on the category  $  {\mathcal C} $), 
then clauses c) and g) have to be modified in order to take into account the covering families of the topology; for example, c) becomes

c')  $  W _  \alpha  ( B \lor C) = \textrm{ T }  \huL ^  \rightharpoonup   $
there exists a covering family of morphisms with domain  $  \alpha $, 
such that for every  $  f $
in the family either  $  W _ {cod  f }  ( B) = \textrm{ T } $
or  $  W _ {cod  f }  ( C) = \textrm{ T } $.

The resulting interpretation is commonly called Kripke–Joyal semantics (after A. Joyal).

For more detailed accounts, see [[#References|[a1]]] or [[#References|[a2]]].

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  R.I. Goldblatt,   "Topoi: the categorial analysis of logic" , North-Holland  (1979)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  J.L. Bell,   "Toposes and local set theories" , Oxford Univ. Press  (1988)</TD></TR><TR><TD valign="top">[a3]</TD> <TD valign="top">  M.A.E. Dummett,   "Elements of intuitionism" , Oxford Univ. Press  (1977)</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  S. Kripke,   "Semantical considerations on modal and intuitionistic logic"  ''Acta Philos. Fennica'' , '''16'''  (1963)  pp. 83–94</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  S.A. Kripke,   "Semantical analysis of intuitionistic logic, I"  J.N. Crossley (ed.)  M.A.E. Dummett (ed.) , ''Formal systems and recursive functions'' , North-Holland  (1965)  pp. 92–130</TD></TR></table>