Supplement to Actualism
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.