An Informal Derivation of NE! from □SA and CBF

Suppose some property necessarily holds of everything; more formally put, that, for some atomic formula φ with ‘x’ free, ^⌈□∀xφ^⌉ is true. (φ might be ‘x=x’, expressing the property being self-identical, for example — in this case, of course, ‘□∀x x=x’ is provable in SQML. Or it might simply be the formula ‘Px’, where ‘P’ is assumed to express some arbitrary property that necessarily holds of everything.) From this, CBF yields ^⌈∀x□φ^⌉. By universal instantiation we have ^⌈□φ^⌉. Then we have the following instance of □SA (where n=0 in that schema): ^⌈□(φ → E!x)^⌉. By the K axiom schema we have ^⌈□φ → □E!x^⌉, and hence ^⌈□E!x^⌉, i.e., NE!.

Note that, even in a language without identity, existence can be expressed our the existence predicate ‘E!’ is taken to be a primitive of the language: At each world, its extension is simply taken to be the class of all individuals and it can be axiomatized in the logic for the language with the sentence ‘∀xE!x’. SA and □SA would take exactly the same forms in this language and the derivation above would still go through.