 That is, intuitively, to say that a statement is possible is just to say that its negation isn’t necessary. The structural similarity between \(\Diamond\textbf{Def}\) and ∃Def should be unsurprising given that, semantically, the necessity operator \(\Box\) is literally a universal quantifier over the set of worlds. Accordingly, it follows from \(\Diamond\textbf{Def}\) and the semantic clause for necessitations that