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.

Copyright © 2014 by
Christopher Menzel <>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free

The SEP would like to congratulate the National Endowment for the Humanities on its 50th anniversary and express our indebtedness for the five generous grants it awarded our project from 1997 to 2007. Readers who have benefited from the SEP are encouraged to examine the NEH’s anniversary page and, if inspired to do so, send a testimonial to