Logic for Computer Scientists/Modal Logic/Kripke Semantics

< Logic for Computer Scientists‎ | Modal Logic

Definition 1Edit

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  .

Lemma 1Edit

The operators   and   are dual, i.e. for all formulae   and all frames  , the equivalence   holds.