Logic for Computer Scientists/Modal Logic/Kripke Semantics

From Wikibooks, open books for an open world
Jump to navigation Jump to search

Definition 1[edit | edit source]

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[edit | edit source]

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