Logic for Computer Scientists/Modal Logic/Kripke Semantics

Definition 1 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 1 The operators and are dual, i.e. for all formulae and all frames , the equivalence holds.