 To illustrate the workings of this framework, consider NC, \(\OB p \rightarrow \neg \OB \neg p\). This is valid in this framework because of seriality. For suppose that \(\OB p\) holds at any world \(i\) in any model. Then each \(i\)-accessible world is one where \(p\) holds, and by the seriality of accessibility, there must be at least one such world. Call it \(j\). Now we can see that \(\neg \OB \neg p\) must hold at \(i\) as well, for otherwise, \(\OB \neg p\) would hold at \(i\), in which case, \(\neg p\) would have to hold at all the \(i\)-accessible worlds, including \(j\). But then p as well as \(\neg p\) would hold at \(j\) itself, which is impossible (by the semantics for “\(\neg\)”). The other axioms and rules of SDL can be similarly shown to be valid, as can all the principles listed above as derivable in SDL.