(a misattribution in the original post is corrected here)

Harvey Friedman wrote:

Virtually noone thinks that there is such a thing that leads to NF. (Do you
mean NFU?) If you have such a thing, surely you can explain it *carefully*
on the fom, at least enough so that one can get a feel for it.

Holmes replies:

I do not think that there is such a thing (known) which leads to NF.
If I had such a thing I could build a model of NF.  However, there is
such a thing which leads to the comprehension scheme of NF (stratified
comprehension) which is the same as the comprehension scheme of NFU.
(It is perhaps worth observing that Marcel Crabbe has shown that SC
(stratified comprehension without any extensionality axiom) interprets
NFU; you can get weak extensionality from no extensionality in this
context).

Friedman asks for a "careful" exposition.  This follows.

We assume the existence of a domain of objects.  If we are going to do
set theory with these objects, this means that we are going to assign
extensions to some of these objects.

An extension (a bare collection of objects) is characterized precisely
by its elements.  We are presumably developing set theory so as to
study properties of collections.

A set as implemented in our set theory has an additional feature over
and above its extension: when a set is implemented, a particular
object is associated with an extension, so we have a structure which
can be described as "an extension with a label" rather than a bare
extension.

The motivation to which we appeal is the abstract data type notion
from computer science: here we are implementing an abstraction
(collections of objects) with an implementation (collections of
objects plus a "label") which has features (the label, and any
relations between elements of the extension and the label) which are
not features of the abstraction being implemented.  Operations on the
abstraction should not use accidental features of the implementation.

Here is an example.  Consider the "set" Delta = "the set of all sets
which are members of themselves".  Please note that this is not a
paradoxical collection; it does exist in positive set theories!  An
object x will be part of the extension associated with Delta iff the
extension associated with x includes the object x itself.

We claim that the specification of Delta violates the security of the
data type "collection" as implemented by "labelled collections".  The
fact that the label x is the same as one of the objects in the
collection it labels is not a property of the extension labelled by x;
this can easily be seen by observing that we could permute the
labelling scheme, choosing an object y which is not an element of this
extension as the new label for this extension and letting x label the
old extension of y.

Notice that this objection can be phrased before ever considering the
question "Is Delta an element of Delta?" or the worse question about
the complement of Delta (the Russell class).  The paradoxes serve to
reinforce an _a priori_ objection to these set definitions.

An object can be considered as a bare object in this scheme.  It can
be considered as representing an extension (a collection).  Objects
can also be considered in a sequence of further roles, one for each
concrete natural number: role 0 = objects, role 1 = collections, role
2 = collections of collections, role 3 = collections of collections of
collections, etc.

Features of one and the same object considered in different roles are
related only by the accident of the particular labelling of extensions
by objects used.  So the specification of a property of collections
can be regarded as respecting the security of the data type
"collection" (or of "collection of collections, etc.) only if each
object mentioned in such a specification is considered in exactly one of
its roles in the specification.  The problem with the specification
"the set of all x such that x is an element of x" is that x appears in
both role 0 and role 1 in the formula "x is an element of x" (or
perhaps role 17 and role 18 -- in any event, in two successive roles).
But this is precisely the criterion of stratified comprehension.  The
roles are of course related to the types in Russell's theory of types
as simplified by Ramsey, but here they are treated (as the semantics
of NFU requires) as different ways to view the same object rather than
different sorts of object.

Some support for this idea is provided by a theorem of Thomas
Forster to the effect that the stratified predicates are precisely
those which are preserved by all redefinitions of the membership
relation by permutation (x \in_{new} y defined as x \in \pi(y), where
\pi is a permutation) such that \pi and \pi_{-1} preserve sets, sets
of sets, sets of sets of sets, etc. in a suitable sense.  This is
found in Forster's book "Set theory with a universal set", Oxford logic
guides no. 20 or 31.

NF is not motivated here because there is no particular reason to
believe that we can ensure that all objects represent distinct
collections.  But SC is motivated, and thus NFU.

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