A Kripke frame is a pair , where is a
non-empty set (of possible worlds) and a binary relation on .
We write iff and we say that world is accessible
from world , or that is reachable from , or that is a
successor of .
A Kripke model is a triple , with and
as above and is a mapping , where
is the set of propositional variables. is intended to be
the set of worlds at which is true under the valuation .
Given a model and a world , we define the
satisfaction relation by:
We say that satisfies iff (without mentioning the
valuation ). A formula is called satisfiable in a model , iff there exists some , such that . A formula
is called satisfiable in a frame , iff there exists
some valuation and some world , such that .
A formula is called valid in a model , written
as iff it is true at every world in . A formula
is valid in a frame , written as iff it is valid in all models .