Editing New Foundations (section)

=== NFU and other variants ===
'''NF with [[urelement]]s''' ('''NFU''') is an important variant of NF due to Jensen{{sfn|Jensen|1969}} and clarified by Holmes.{{sfn|Holmes|1998}} Urelements are objects that are not sets and do not contain any elements, but can be contained in sets. One of the simplest forms of axiomatization of NFU regards urelements as multiple, unequal empty sets, thus weakening the extensionality axiom of NF to:
* Weak extensionality: Two ''non-empty'' objects with the same elements are the same object; formally,
:<math display="block">\forall x y w. (w \in x) \to (x = y \leftrightarrow (\forall z. z \in x \leftrightarrow z \in y)))</math>
In this axiomatization, the comprehension schema is unchanged, although the set <math>\{x \mid \phi(x)\}</math> will not be unique if it is empty (i.e. if <math>\phi(x)</math> is unsatisfiable).

However, for ease of use, it is more convenient to have a unique, "canonical" empty set. This can be done by introducing a sethood predicate <math>\mathrm{set}(x)</math> to distinguish sets from atoms. The axioms are then:{{sfn|Holmes|2001}}
* Sets: Only sets have members, i.e. <math>\forall x y. x \in y \to \mathrm{set}(y).</math>
* Extensionality: Two ''sets'' with the same elements are the same set, i.e. <math>\forall y z. (\mathrm{set}(y) \wedge \mathrm{set}(z) \wedge (\forall x. x \in y \leftrightarrow x \in z)) \to y = z.</math>
* Comprehension: The ''set'' <math>\{x \mid \phi(x) \}</math> exists for each stratified formula <math>\phi(x)</math>, i.e. <math>\exists A. \mathrm{set}(A) \wedge (\forall x. x \in A \leftrightarrow \phi(x)).</math>

NF<sub>3</sub> is the fragment of NF with full extensionality (no urelements) and those instances of comprehension which can be stratified using at most three types.  NF<sub>4</sub> is the same theory as NF.

Mathematical Logic (ML) is an extension of NF that includes proper classes as well as sets. ML was proposed by Quine and revised by Hao Wang, who proved that NF and the revised ML are equiconsistent.