 A formula \(\mathtt{\phi}\) is said to be true at \(w\) if \(M, g, w \vDash \mathtt{\phi}\); otherwise it is said to be false at \(w\). By convention \(M, g \vDash \mathtt{\phi}\) means \(M, g, w \vDash \mathtt{\phi}\) for every element \(w\) of \(W\) and \(M \vDash \mathtt{\phi}\) means \(M, g \vDash \mathtt{\phi}\) for every assignment \(g\). A formula \(\mathtt{\phi}\) is valid in a frame if and only if \(M \vDash \mathtt{\phi}\) for any model \(M\) that is based on the frame in question. A formula \(\mathtt{\phi}\) is valid in a class of frames \(F\) if and only if \( \mathtt{\phi}\) is valid in any frame in \(F\). A formula \(\mathtt{\phi}\) is valid if and only if \(\mathtt{\phi}\) is valid in the class of all frames. The definition of satisfiability is left to the reader.