Kripke model

English

Etymology

Named after Saul Kripke.

Noun

Kripke model (plural Kripke models)

1. (logic) A Kripke frame together with either one of the following: (1) a function associating each of the frame's worlds to a set of prime formulae which are "true" for the given world, (2) a function associating each prime formula to a set of worlds for which the prime formula is "true", (3) a forcing relation between worlds and prime formulae. Additionally, there is a set of rules for deducing (from the given function or relation) what formulae are forced to be true by a given world. (The set of rules depends on which logic the Kripke model is being applied to, whether one of several modal logics or intuitionistic logic). For intuitionistic logic the forcing relation satisfies a persistence relation, namely, if world w forces proposition p, then all worlds accessible from w also force p.

   A formula is intuitionistically valid iff it is forced true by every world of every Kripke model.

   A terminal world of a Kripke model (for intuitionistic logic) has a forcing relation equivalent to a classical model/interpretation.

   If a given world (in a Kripke model (for intuitionistic logic)) forces neither $A$ nor $\neg A$ then there is some possible "future" world (accessible from the "present" one) in which $A$ is forced true. In particular, if $A$ eventually becomes forced somewhere along any possible time thread (towards the "future"), then the present world would force $\neg \neg A$ to be true, but if this does not happen there there exists some possible future world in which $\neg A$ becomes true.

Related terms

• Kripke semantics