 Semantically, the formula \([F!]G\) is interpreted in a Kripke model as follows: to say that \([F!]G\) is true means that, whenever F is true, G is true after we eliminate all not-F possibilities (and all arrows to and from these possibilities). This makes sense: since the public announcement of F is completely trustworthy, all agents respond by collectively eliminating all non-F possibilities from consideration. So to see what obtains after a public announcement of F occurs, we eliminate the non-F worlds and then see what is true in the resulting situation. Formally, \(\eqref{PAL}\)-formulas are evaluated as an extension of the binary truth relation \(\models\) between pointed Kripke models and \eqref{ML}-formulas (defined in  Appendix A)  as follows: given a Kripke model \(M=(W,R,V)\) and a world \(w\in W\), 