## 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.