A set theory introduced by W.V.O. Quine in 1937. Not yet proved consistent, as far as I know.

See <http://math.boisestate.edu/~holmes/holmes/nf.html>.

NFU ("New Foundations with Urelemente"), and several other NF variants, '''have''' been proven consistent; see <http://projecteuclid.org/Dienst/UI/1.0/Summarize/euclid.ndjfl/1093636013>. "Urelemente" is the German word for "atoms", i.e. entities that do not have any members or structure, but are distinct from each other (like Lisp atoms). These are quite useful for ComputerScience applications, e.g. you can use NFU as a type system in which some of the language's objects are modelled as Urelemente, and with the types '''Type''' and '''Any''' (TopType) corresponding to the SetOfAllSets and the UniversalSet respectively. See also SemanticSubtyping.

The WatsonTheoremProver is based on NFU.

----
CategoryMath