 It is clear where the problem lies: the universal instantiation schema Q2 is invalid in KQML! To see this in the particular case of line 1, suppose that \(\forall \sfx \Box \neg \sfB\sfx\) is true in (i.e., true at the “actual world” of) a given Kripke interpretation \(\calK\) with individuals \(D\) and worlds \(W\). Then, by  the quantificational clause  in the definition of truth at a world in Kripke’s semantics, everything that exists in the “actual world” \(w^\ast\) of \(\calK\) is not in the extension of \(\sfB\) at any world \(u\) in \(W,\) i.e., for all \(a \in \textit{dom}(w^\ast)\) and for all \(u \in W,\) \(a \notin \sfB^\calK_{u}\). Recall, however, that the value \(\sfx^\calK\) assigned to \(\sfx\) can be anything in the set \(D\) of individuals of \(\calK\); in particular, \(\sfx^\calK\) might not exist in \(w^\ast\) and, hence, might well be in the extension of \(\sfB\) at some other world of \(\calK,\) in which case \(\Box\neg \sfB\sfx\) will be false in  \(\calK.\)[56]