Quine's original motivation for NF was purely as a syntactical
variation on the theory of types.  He noticed that in Russell's
original theory of types, as simplified by Ramsey, every theorem and
definable object has a precise analogue obtained by raising every type
index by one.  He found this "hall-of-mirrors" effect, as well as the
notational cumbersomeness of type superscripts, to be distasteful, and
found by experiment that abandoning the types while retaining the
restriction on comprehension that only those instances of
comprehension which are "typable" are provided did not seem to lead to
contradiction.

Specker proved model theoretical results showing that (as one might
expect) the consistency of NF is equivalent to the existence of models
of the theory of types in which the structure with types 0,1,2... is
isomorphic to the structure with types 1,2,3...  Specker also proved
that NF as formulated by Quine disproves the Axiom of Choice.  No one
has come close to constructing a model of the theory of types with an
isomorphism as described above; on the other hand, no one has shown
that NF is any stronger than the theory of types with the axiom of
infinity (infinity is an immediate corollary of the negation of
choice; Quine's argument for infinity in NF given in the original NF
paper is NOT valid).

Jensen showed in 1969 that NFU, in which extensionality is weakened to
allow urelements, is consistent, and is moreover consistent with
Infinity and Choice (and does not prove infinity, though all models of
NFU are infinite).  He also showed (in ZFC) that NFU has models in
which the ordinals up to alpha are standard, for any ordinal alpha.
NFU (extended with strong axioms of infinity as needed) is an entirely
sensible set theory, on which mathematics could be founded as readily
as on ZFC.

Maurice Boffa described the following construction of a model of NFU,
which is natural in the ZFC context: take a nonstandard model of
enough of ZFC (it doesn't take very much) with an external
automorphism j moving a (necessarily nonstandard) ordinal alpha
upward.  The model of NFU will have domain V_alpha (level alpha of the
cumulative hierarchy) and membership relation x \in_NFU y defined as
"x \in j(y) and j(y) \in V_{alpha+1}.  It is straightforward to
establish (using a variation on Specker's model theory results about
NF) that a model of NFU (with many urelements) is obtained in this way.

The proposal that NFU be used as a foundation does require some
attention to the motivation of the set notion of NFU in its own terms.
Here is a motivation which I have proposed: set theory is an attempt
to represent collections of objects as objects themselves.  The
motivation appeals to the concept of data type abstraction.  The
abstraction being implemented is "collection of objects" (strictly
speaking, "class", rather than "set"), while a set is a collection of
objects identified with a particular object; it may be thought of as a
class with a label attached.  We are only supposed to be interested in
properties of collections of objects; properties of the implementation
of a given collection which depend on the particular choice of object
to represent the collection should not be of interest to us.  One such
property is "x is an element of x"; this says "the object used to
represent the collection is one of the objects in the collection";
this is not a property of the implemented collection, but of its
implementation.  We can consider objects per se, objects as
representing collections, and we can also consider objects as
representing collections of collections (by considering the
collections represented by eache element of the collection they
represent), and so forth (this hierarchy of aspects under which an
object can be viewed is the same as the hierarchy of types in
Russell's theory, but here they are different ways to view the same
object rather than different sorts of object).  "Data type security"
suggests that the "specification" of any set we are interested in
should involve any given object under only one of these aspects; the
relationship between the different aspects of an object is a feature
of the implementation of sets rather than of sets themselves.  This
turns out to be precisely the criterion of stratified comprehension;
notice that it provides a reason to reject the problematic set
definition {x | x \not\in x} a priori, before discovering the paradox.
Note that nothing in this picture suggests that every object should be
used to represent a collection of objects; there is no commitment to
extensionality, so NFU is motivated here.  NF would require further
motivation.

This method of restricting comprehension is incompatible in spirit
with the restriction on comprehension used in ZFC.  The axiom of
separation of ZFC is false in NFU, since there is a universal set in
NFU.  The definition of ordinals used in ZFC cannot be used in NFU,
because it relies essentially on unstratified notions.  In general,
any recursion or induction on the membership relation (as in the
construction of the cumulative hierarchy in ZFC) is ruled out in NFU.
The natural way to define ordinals in NFU is as isomorphism types of
well-orderings.  The natural numbers, and cardinal numbers in general,
are defined using Frege's definition.

We have seen above that NFU can be interpreted in ZFC; it turns out
that Zermelo style set theory can be interpreted readily in NFU as
well.  For example, if we assume that the universe V has size an
inaccessible cardinal, the collection of isomorphism types of
well-founded extensional relations with domain smaller than the
universe makes up a model of ZFC with a natural "membership relation".
(The system NFU + |V| is inaccessible is actually stronger than ZFC;
it proves the existence of many inaccessibles).

NFU and ZFC rely on different notions of set, but they turn out to
reveal essentially the same mathematical universe.  Each theory
interprets the other readily, and the choice between them is in my
view a matter of taste.  These remarks do not apply to NF itself,
which represents a rather peculiar view of things.  But the
peculiarity of NF lies entirely in its use of strong extensionality;
NFU uses precisely the same comprehension scheme as NF.

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes@math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes