That is, informally, if there could be something satisfying any given description \(\varphi,\) then there is something that could satisfy that description, a thing that is possibly \(\varphi.\) The validity of BF in SQML rests on two facts: first, that in the model theory of SQML (as in all varieties of possible world semantics), the possibility operator \(\Diamond\) is literally an existential quantifier ranging over all possible worlds; and second, that, in evaluating an existentially quan