Noun
Kripke model (plural Kripke models)
(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).
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
{\displaystyle A}
nor
¬
A
{\displaystyle \neg A}
then there is some possible "future" world (accessible from the "present" one) in which
A
{\displaystyle A}
is forced true. In particular, if
A
{\displaystyle A}
eventually becomes forced somewhere along any possible time thread (towards the "future"), then the present world would force
¬
¬
A
{\displaystyle \neg \neg A}
to be true, but if this does not happen there there exists some possible future world in which
¬
A
{\displaystyle \neg A}
becomes true.