Namespaces
Variants
Actions

Difference between revisions of "Kripke models"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (tex encoded by computer)
Line 1: Line 1:
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558501.png" /> is given by
+
<!--
 +
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.
 +
-->
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558502.png" /></td> </tr></table>
+
{{TEX|auto}}
 +
{{TEX|done}}
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558503.png" /> is a non-empty set (of "worlds" ,  "situations" ); <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558504.png" /> is a binary relation on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558505.png" /> (for example, for the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558506.png" /> of [[Intuitionistic logic|intuitionistic logic]], <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558507.png" /> is a partial order; for the modal system (cf. [[Modal logic|Modal logic]]) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558508.png" /> it is a pre-order; for the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k0558509.png" /> it is an equivalence relation); <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585010.png" /> is a mapping which associates with each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585011.png" /> a non-empty domain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585012.png" /> such that, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585013.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585014.png" />; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585015.png" /> is a valuation which associates with each individual constant <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585016.png" /> of the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585017.png" /> an element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585018.png" />, and with each individual variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585019.png" /> an element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585020.png" />; for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585021.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585022.png" /> associates with each propositional variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585023.png" /> a truth value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585024.png" /> (for the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585025.png" /> it is also stipulated that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585026.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585027.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585028.png" />); with each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585029.png" />-placed (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585030.png" />) predicate symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585031.png" /> a certain subset <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585032.png" /> (for the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585033.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585034.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585035.png" />); and with each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585036.png" />-placed function symbol <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585037.png" /> a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585038.png" /> from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585039.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585040.png" /> (for the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585041.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585042.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585043.png" /> is the restriction of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585044.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585045.png" />).
+
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
  
For any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585046.png" /> and any formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585047.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585048.png" /> such that for each free variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585049.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585050.png" /> one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585051.png" />, the truth value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585052.png" /> is defined inductively. For the system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585053.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585054.png" /> is defined as follows:
+
$$
 +
= ( S, R, D, W),
 +
$$
  
a) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585055.png" /> is an atomic formula, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585056.png" /> is already defined in the model;
+
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  $).
  
b) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585057.png" />;
+
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:
  
c) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585058.png" />;
+
a) if  $  A $
 +
is an atomic formula,  $  W _  \alpha  ( A) $
 +
is already defined in the model;
  
d) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585059.png" /> (for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585060.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585061.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585062.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585063.png" />);
+
b)  $  W _  \alpha  ( B \& C) = \textrm{ T }  \rightharpoonup ^  \huL    ( W _  \alpha  ( B) = \textrm{ T }  \textrm{ and }  W _  \alpha  ( C) = \textrm{ T } ) $;
  
e) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585064.png" /> (for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585065.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585066.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585067.png" />);
+
c)  $  W _  \alpha  ( B \lor C) = \textrm{ T }  \rightharpoonup ^  \huL    ( W _  \alpha  ( B) = \textrm{ T }  \textrm{ or }  W _  \alpha  ( C) = \textrm{ T } ) $;
  
f) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585068.png" /> (for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585069.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585070.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585071.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585072.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585073.png" />);
+
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 } $);
  
g) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585074.png" /> (there exists a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585075.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585076.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585077.png" />)
+
e)  $  W _  \alpha  ( \neg B) = \textrm{ T }  \rightharpoonup ^  \huL  $(
 +
for any  $  \beta \in S $,
 +
if  $  \alpha R \beta $,
 +
then  $  W _  \beta  ( B) = \textrm{ F } $);
  
(here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585078.png" /> means that the valuation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585079.png" /> coincides with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585080.png" /> everywhere, except possibly on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585081.png" />). Instead of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585082.png" /> one sometimes writes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585083.png" />.
+
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 } $);
  
For modal logics, the definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585084.png" /> in cases d, e and g is different:
+
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 } $)
  
d') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585085.png" />;
+
(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 $.
  
e') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585086.png" />;
+
For modal logics, the definition of  $  W _  \alpha  ( A) $
 +
in cases d, e and g is different:
  
g') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585087.png" /> (for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585088.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585089.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585090.png" />);
+
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
 
and, in addition, one requires
  
h) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585091.png" /> (for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585092.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585093.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585094.png" />).
+
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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585095.png" /> is said to be true in a Kripke model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585096.png" /> (written <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585097.png" />) if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585098.png" /> for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k05585099.png" />. For each of the systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850100.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850101.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850102.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850103.png" /> are in general different, since the formula
+
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
  
<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850104.png" /></td> <td valign="top" style="width:5%;text-align:right;">(*)</td></tr></table>
+
$$ \tag{* }
 +
\forall  x  ( A \lor B ( x))  \supset  A \lor \forall  x  B ( x),
 +
$$
  
where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850105.png" /> is not free in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850106.png" />, is not deducible in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850107.png" />, but it is true in all Kripke models with constant domain. The system obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850108.png" /> by adding the scheme (*) is complete relative to Kripke models with constant domain (see [[#References|[3]]]). The propositional fragment of each of the systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850109.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850110.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850111.png" /> 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.
+
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]]).
 
The concept of a  "Kripke model" , due to S.A. Kripke, is related to that of forcing (see [[Forcing method|Forcing method]]).
Line 45: Line 158:
 
====References====
 
====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>
 
<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====
 
====Comments====
Kripke models for intuitionistic logic are a special case of topos-theoretic models (cf. also [[Topos|Topos]]). Specifically, the function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850112.png" /> in the definition may be regarded as a pre-sheaf (i.e., a set-valued functor) on the partially ordered set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850113.png" />; the function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850114.png" /> equips this pre-sheaf with a structure for the given language, internally in the topos of pre-sheaves on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850115.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850116.png" /> is replaced by an arbitrary small category <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850117.png" />) — one has only to replace the quantification over nodes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850118.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850119.png" />, which occurs in clauses d), e) and f), by a quantification over morphisms of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850120.png" /> with domain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850121.png" />. However, if one considers models in a topos of sheaves (that is, if one introduces a Grothendieck topology on the category <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850122.png" />), 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
+
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') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850123.png" /> there exists a covering family of morphisms with domain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850124.png" />, such that for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850125.png" /> in the family either <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850126.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/k/k055/k055850/k055850127.png" />.
+
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).
 
The resulting interpretation is commonly called Kripke–Joyal semantics (after A. Joyal).

Revision as of 22:15, 5 June 2020


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 } \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 [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).

References

[1a] S.A. Kripke, "A completeness theorem in modal logic" J. Symbolic Logic , 24 (1959) pp. 1–14
[1b] S.A. Kripke, "The undecidability of monadic modal quantification theory" Z. Math. Logik Grundl. Math. , 8 (1962) pp. 113–116
[1c] S.A. Kripke, "Semantical analysis of modal logic, I" Z. Math. Logik Grundl. Math. , 9 (1963) pp. 67–96
[1d] 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
[2] K. Schütte, "Vollständige Systeme modaler und intuitionistischer Logik" , Springer (1968)
[3] S. Görnemann, "A logic stronger than intuitionism" J. Symbolic Logic , 36 (1971) pp. 249–261
[4] P.J. Cohen, "Set theory and the continuum hypothesis" , Benjamin (1966)

Comments

Kripke models for intuitionistic logic are a special case of topos-theoretic models (cf. also 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) 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 [a1] or [a2].

References

[a1] R.I. Goldblatt, "Topoi: the categorial analysis of logic" , North-Holland (1979)
[a2] J.L. Bell, "Toposes and local set theories" , Oxford Univ. Press (1988)
[a3] M.A.E. Dummett, "Elements of intuitionism" , Oxford Univ. Press (1977)
[a4] S. Kripke, "Semantical considerations on modal and intuitionistic logic" Acta Philos. Fennica , 16 (1963) pp. 83–94
[a5] 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
How to Cite This Entry:
Kripke models. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Kripke_models&oldid=47526
This article was adapted from an original article by S.K. Sobolev (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article