 Classical modal logics have a semantics in terms of so-called minimal models, also known as neighbourhood models. A neighbourhood model is a structure \(\cal M\) \(=\) \((W, N, v)\), where \(W\) is a non-empty set of possible worlds, \(N\) is a function assigning to every \(w\) from \(W\) a set \(N(w)\) of subsets of \(W\), called neighbourhoods of \(w\), and \(v\) is a valuation function mapping atomic formulas to the set of worlds where they are true. Let \(\llbracket A\rrbracket\) be the set of worlds at which formula \(A\) is true. Then \( \Box A\) is defined to be true at a world \(w\) in model \(\cal M\) (in symbols: \({\cal M}, w \models \Box A\)) iff \(\llbracket A\rrbracket \in N(w)\).