I have an argument of this kind for the stratification criterion of
"New Foundations" (which I do not use to support NF itself as a
foundation; but NFU has the same criterion for comprehension and is a
sensible theory).  [Aside to Harvey: I gave the wrong answer to a
question you asked me about models of NFU a while ago; natural models
of NFU do not have automorphisms -- they have endomorphisms, as does
PA, for example, which is not problematic]

The argument can be expressed in terms of the criteria for an abstract
data type.  A set is a collection of objects; it is also an object
itself.  What we are interested in when we are given a set is its
extension alone (which objects are its members); but a set has further
features in which we "should not" be interested -- any relations
between the object which it _is_ and the objects which it has as
elements.  The abstraction under consideration is a collection of
objects; the implementation of the abstraction is a collection of
objects associated with a further object (with which it is to be
identified).

The (non-paradoxical) predicate of x expressed by "x \in x" is an
example of a property of the implementation of a set which is not a
property of the abstraction which the set is to implement.  It is not
a property of the extension but of the relation between the object
identified with the extension and the objects which belong to the
extension.  We object to its paradoxical complement for the same
reason, and this objection can be formulated prior to any
consideration of paradox.  

In the sentence "x \in x", x appears with two different "roles"; it
appears as a possible element of an extension under consideration, and
it also appears as the object being used to represent that extension.
Further consideration of specifications of sets leads to the
recognition of a hierarchy of roles: an object can appear as a "mere"
object, as representing a collection of mere objects, as representing
a collection of collections of mere objects, etc.  These roles are
recognizable as the types of Russell's type theory as simplified by
Ramsey, but they are not in this context different kinds of object,
but different ways of viewing the same object.

Specifications which respect the abstraction "set" as understood here
are those in which any object involved in the specification is
considered via only one of its "roles"; we do not allow ourselves
access to information about the relationship between the different
roles of the same object (information about the details of how we
associate objects with extensions).  But this is precisely the
criterion of stratified comprehension found in NF or NFU.

This is an attempt to answer the criticism of stratified comprehension
as a syntactical trick (which it certainly was for Quine!).  There is
mathematical support for it in a theorem of Forster that the
stratified formulas are exactly those which are unperturbed by
redefinitions of the membership relation by permutation statisfying a
certain natural restriction.  A redefinition of the membership
relation by permutation (x \in_{new} y iff x \in \pi(y), \pi a
permutation) is a change in the implementation of the set abstraction
which should not be visible to predicates which respect the
abstraction; the restriction is that not only collections of bare
objects, but collections of collections of bare objects etc. need to
be preserved by \pi (see Forster's book "Set theory with a universal
set", Oxford logic guides no. 20 or 31, for details).

Now, of course, there is a problem: stratified comprehension as a
criterion rules out very popular sets in the ZFC hierarchy, such as
infinite von Neumann ordinals and stages of the cumulative hierarchy
with infinite index!  It isn't that they are actually forbidden, but
that the stratification criterion does not specifically allow them.

In NF or NFU, one defines cardinals as equivalence classes of sets
under equinumerousness (in particular, Frege's definition of natural
number succeeds!) and ordinals as equivalence classes of
well-orderings under similarity.  The existence of many von Neumann
ordinals can be recovered by a permutation technique, but it turns out
that not all ordinals can correspond to von Neumann ordinals (the big
ordinals, such as the order type of On itself, cannot correspond to
von Neumann ordinals; for those who know the terminology, it is
possible to get the strongly Cantorian ordinals to correspond to von
Neumann ordinals, and this is the best one can do).

The difficulty with von Neumann ordinals and stages of the cumulative
hierarchy points to the fact that I wasn't actually talking about the
right abstraction above.  The abstraction implemented by sets of ZFC
is not the bare abstraction "collection" as I described it; it is
something more like "well-founded extensional graph" (we want to see
not only elements, but also elements of elements, etc., which violates
the restrictions of the data type "collection" as I described it
above; well-foundedness of the graphs comes from the intuition of the
cumulative hierarchy).  In NFU , one can develop the theory of
isomorphism classes of well-founded extensional relations and recover
an interpretation of a Zermelo-style set theory; one needs to add
strong axioms of infinity to NFU to get a theory as strong as ZFC
(there are strong axioms of infinity natural for NFU which give
considerably more strength than ZFC; Solovay has very nice results
along these lines).

Foundations based on NFU (plus at least Infinity and Choice, and
probably more strong axioms) are useful in this context as providing a
historically (partially) independent alternative foundation.  They
provide a reality check on commonly made false assertions about the
paradoxes: big collections like the universe or the set of all
Russell-Whitehead ordinals are not paradoxical (the von Neumann
ordinals can't make up a set), and Frege's development of arithmetic
can be made to succeed.  On the other hand, closer examination reveals
that the world uncovered in NFU and its natural extensions is the same
in its essential features as the world of ZFC.  Each kind of
foundation interprets the other readily (suitable extensions of NFU
interpret ZFC slightly more easily than ZFC interprets NFU and
extensions).  They don't disagree on logical fundamentals and they are
both set theories.

Summary of basic results about NF and NFU: the consistency of Quine's
original system NF (proposed 1937) remains an open question.  Specker
showed in 1954 that NF disproves AC (this caused a considerable
decline in interest!)  Jensen defined NFU in 1969 and showed that it
is consistent (rel ZFC) and can be extended with Infinity, Choice and
stronger axioms.  Grishin (1969) and Marcel Crabb\'e (1983) showed the
consistency of other interesting subtheories of NF.  Good books are
Rosser's Logic for Mathematicians, in which it is shown that
mathematics can be founded on NF + denumerable choice (which is not
known to be inconsistent; Rosser was writing just before Specker
disproved full choice, and his entire development can be adapted to
NFU with minimal changes) and Thomas Forster's recent "Set theory with
a universal set", Oxford logic guides no. 20 or 31.  My "elementary set
theory text" using NFU will appear shortly.  References to all of this
(the exhaustive bibliography of Forster's book on-line!)  and a more
extensive summary can be found on the New Foundations Home Page, which
can be reached from my home page (see .signature).

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