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 } $);

and, in addition, one requires

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 [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 } \leftrightharpoons $ 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