 Kripke’s solution here—once again borrowing from Quine (1951)—jettisons both Gen and Nec and cleverly incorporates the desired effects of both rules directly into his specification of the logical axioms of his deductive system—which, of course, we will call KQML. To express the solution clearly, say that a formula is closed if it contains no free variable occurrences, and define a closure of a formula \(\varphi\) to be any closed formula resulting from prefixing a (possibly empty) string of universal quantifiers and necessity operators, in any order, to \(\varphi\). Then, given a language \(\scrL_\Box\) without any individual constants, any closure of any instance of any of the following schemas is an axiom of KQML: