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 is given by
![]() |
where is a non-empty set (of "worlds" , "situations" );
is a binary relation on
(for example, for the system
of intuitionistic logic,
is a partial order; for the modal system (cf. Modal logic)
it is a pre-order; for the system
it is an equivalence relation);
is a mapping which associates with each
a non-empty domain
such that, if
, then
;
is a valuation which associates with each individual constant
of the language
an element
, and with each individual variable
an element
; for each
,
associates with each propositional variable
a truth value
(for the system
it is also stipulated that if
and
, then
); with each
-placed (
) predicate symbol
a certain subset
(for the system
, if
, then
); and with each
-placed function symbol
a function
from
to
(for the system
, if
, then
is the restriction of
to
).
For any and any formula
of
such that for each free variable
in
one has
, the truth value
is defined inductively. For the system
,
is defined as follows:
a) if is an atomic formula,
is already defined in the model;
b) ;
c) ;
d) (for any
, if
and
, then
);
e) (for any
, if
, then
);
f) (for any
and
, if
and
, then
);
g) (there exists a
such that
and
)
(here means that the valuation
coincides with
everywhere, except possibly on
). Instead of
one sometimes writes
.
For modal logics, the definition of in cases d, e and g is different:
d') ;
e') ;
g') (for any
, if
, then
);
and, in addition, one requires
h) (for any
, if
, then
).
A formula is said to be true in a Kripke model
(written
) if
for any
. For each of the systems
,
and
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
are in general different, since the formula
![]() | (*) |
where is not free in
, is not deducible in
, but it is true in all Kripke models with constant domain. The system obtained from
by adding the scheme (*) is complete relative to Kripke models with constant domain (see [3]). The propositional fragment of each of the systems
,
and
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 in the definition may be regarded as a pre-sheaf (i.e., a set-valued functor) on the partially ordered set
; the function
equips this pre-sheaf with a structure for the given language, internally in the topos of pre-sheaves on
, 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
is replaced by an arbitrary small category
) — one has only to replace the quantification over nodes
such that
, which occurs in clauses d), e) and f), by a quantification over morphisms of
with domain
. However, if one considers models in a topos of sheaves (that is, if one introduces a Grothendieck topology on the category
), 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') there exists a covering family of morphisms with domain
, such that for every
in the family either
or
.
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 |
Kripke models. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Kripke_models&oldid=47526