 With these modifications in place, Kripke is able to demonstrate that his deductive system KQML is sound and complete for closed formulas relative to his semantics. Soundness, in particular, tells us that no invalid formula is provable in the system. Hence, since BF, CBF, and \(\Box\textbf{N}\) are all invalid in KQML, soundness guarantees that they are all unprovable in KQML.