FOM: what is the view of sets in NF or NFU?

[holmes@catseye.idbsu.edu]

Simpson said (speaking of alternative foundational schemes):

First, NF.  

Aspect 1.  NF is interpretationally rich in the same sense and for the
same reasons as ZFC.  But nobody has calibrated exactly how rich it
is, in terms of the usual ordering of large cardinal axioms.  Type
theory is interpretable in NF, but it remains unknown whether ZFC is
interpretable in NF, or whether NF is interpretable in ZFC.  Much more
is known about calibrating NFU, i.e., NF with urelements.  Solovay has
calibrated NFU + infinity + choice + ``small ordinals''.  It turns out
to be almost as rich as ZFC + a weakly compact cardinal.  However,
weakly compact cardinals are relatively puny as large cardinals go,
and it is unclear (to me at least) how the beefier large cardinals fit
in with NF.  Perhaps some NFists could explain.

I comment:

I would conjecture that NF is either inconsistent or precisely as
strong as the theory of types with the axiom of infinity (so as strong
as Mac Lane set theory = Zermelo with bounded comprehension).  NFU +
Infinity is in any event of precisely the strength of Mac Lane set theory
and is mathematically more satisfactory than NF because it allows choice.

The precise strength of NF itself is not really all that relevant:
one would immediately strengthen NF with Rosser's axiom of counting
and probably other strong axioms of infinity; the axiom of "small ordinals"
which I considered for NFU and whose strength Solovay has settled would
be natural for NF and NF + "small ordinals" (if consistent) is stronger
than ZFC.  

The situation for NFU is more clearly understood, as Simpson says.
There is a natural extension of NFU (described in my book and more
formally discussed in a paper to appear in the JSL) which has the
strength of Morse-Kelley plus a primitive predicate of classes which
is a measure on the proper class ordinal (this is in some sense just
short of having a measurable cardinal).  There are strong axioms of
infinity natural for NFU which will give even larger cardinals.

Simpson continued:

Aspect 2.  NF starts with the same naive picture as ZFC (marbles on a
table, etc) but ends up being much less intuitive.  For one thing, NF
does not offer any nice picture of the universe as a hierarchy of
sets, like the cumulative hierarchy of ZFC.  At every turn it seems
necessary to work with an unintuitive syntactic notion, that of
``stratified formula''.  I find this a little off-putting.  Of course
this could be due to my relative unfamiliarity with NF.  Do NFists
claim to have a picture of the NF universe which they find intuitively
appealing?  Does such a picture have any categoricity properties?

I comment:

If NFU offers a picture of things (I attempt to describe one below) it
is not a picture of the universe as a hierarchy of sets; that would
make it essentially the same as ZFC (just at a higher or lower level of
strength).  But the hierarchy of sets that ZFC sees is visible within
NFU (as something else).  Re stratification, see below.  I have no idea
what the picture of the world in NF would be like; I do have a picture
(a couple of different pictures) of what the world of NFU is like, but
I'm not sure what categoricity properties it might have (I think one
would have to strengthen it to make its models in any sense categorical,
and I think that extensions of NFU with categoricity properties would be 
quite interesting if they exist).

Simpson said further in response to Forster:

Thomas Forster 3 Mar 2000 writes:

 > True NF seems to be interpretationally weak, but this doesn't
 > necessarily hold any moral for the view of set theory that it
 > represents.  It might just not represent it very well.

This is a good point.  Maybe we need to get clearer on exactly what
view of sets gives rise to NF.  Then perhaps we will be able to think
of better formal representions of that view, which might turn out to
be interpretationally richer than NF.

So, what is the view of sets reflected (perhaps imperfectly) by NF?
Can this view be described discursively, i.e., in words?  Is it a
conceptually coherent view?  Is it as coherent as, say, the view of
sets that is reflected (perhaps imperfectly) by ZFC?

The ZFC view of sets seems reasonably coherent and has been described
discursively many times, in terms of the well-known cumulative
hierarchy, obtained by transfinite iteration of the power set
operation along the ordinal numbers.  This is in papers by Zermelo,
Fraenkel, von Neumann, Shoenfield, and others.  In addition, the
cumulative hierarchy has interesting categoricity properties which
tend to increase our confidence in the underlying picture.

Is there a discursive description of the NF view of sets that that is
comparably convincing and/or of comparable clarity?  Are there papers
(by Quine and Rosser perhaps) which provide such a description?

Forster replied:

What does tend to happen is that people write articles purporting to 
provide such a story and they get sent to Holmes and me to referee.
So far i have always rejected those i've seen, always on the grounds
that if the story being told were a good one it would come a lot
closer to giving a consistency proof for NF than the document in front
of me did.
   Inasfar as there is a story available at the moment, i think it is
the idea of stratfication, which is a lot more sensible than one
realises.  There is a completeness theorem for stratification, to the
effect that it's an invariance property.   But we've been over this
material before on this list, so presumably this is not what Steve has
in mind.  For all that, i suspect it *is* what he wants.

I comment:

Quine certainly does not give any sensible motivation for NF.  He
developed it as a notational variation on type theory, and (as
motivated by Quine) NF has been fairly described as being the product
of a "syntactical trick".  Rosser didn't say anything about the
motivation of the system, though he did a good job of demonstrating
its practical effectiveness as a foundation for mathematics (just
before the disproof of AC by Specker cast grave doubts on the wisdom
of choosing NF as a foundation, and too soon for the results of Jensen
to show that NFU is consistent, supports Rosser's development just as
well, and admits AC)

However, this does not mean that NF (or NFU) cannot be motivated in a
sensible way.

One motivation which is certainly accessible (for NFU) is to look at
the model constructions.  One can arrive at the conclusion that NFU is
a way of talking about nonstandard models of initial segments of the
cumulative hierarchy with automorphisms that move a level.  This certainly
does not motivate NFU as an autonomous foundation for mathematics, because
it is dependent on the foundational view underlying ZFC (though not on
the full strength of ZFC; bounded Zermelo set theory is enough) plus
some model theory.

With a little care, NFU can be motivated as an autonomous foundation
of mathematics using the same model theory, by working in a different
context.  One can start out with a type theory as one's foundation,
develop the model theory needed for the construction of NFU, and use
this to motivate the collapse of the type hierarchy (and there really
is an intuitive motivation for the collapse of the type hierarchy --
the problem is that it is an intuitive motivation which requires
nontrivial formal justification).  The evaluation of this goes as
follows: the type theory one starts with has a clear intuitive
motivation, but is notationally inconvenient and exhibits a
polymorphism which is annoying and suggests that the type hierarchy
might be collapsible.  The work to show that the type hierarchy CAN be
collapsed is nontrivial (it is not intuitively obvious why NFU is OK,
NF is hard to justify, and NF + Choice is impossible to justify; the
polymorphism looks the same in nonextensional type theory, extensional
type theory, and extensional type theory with AC).  But the work does
not have to be done in ZFC; it can be done in the type theory itself.
Here we have NFU motivated as a foundation for mathematics
independently of ZFC -- as a technical amendment to a prior type
theoretical motivation.  It should be noted that one can also get
bounded Zermelo set theory as a technical amendment to type theory,
by taking a different approach to collapsing the type hierarchy.

There is an "intuitive motivation" for stratified comprehension which
I have presented elsewhere (it has been described on this list, and
the postings in which I described it are available on my home page).
This motivation isn't self-sufficient in the way the justification via
type theory described above is; it would have to be coupled with a
formal development, probably the same one that I describe above.  What
it adds is an indication that one does not need to have an underlying
typed view of things to see the appeal of NF or NFU.

There is a view of what a set is involved here, which is more complex
than the view found in ZFC, but not so complex as to be
incomprehensible.  

The most interesting way to get at this view in this context is to
try to extract it from the formal development of NFU as an autonomous
foundation which I outline above.

One begins with type theory (extensional or nonextensional turns out
not to matter -- the process of amendment suggests that the theory
ought to be retroactively taken to be nonextensional).  Type theory is
a higher order logic: what we refer to as individuals, sets of
individuals, sets of sets of individuals, and so forth, can equally
well be understood as objects, predicates of objects, predicates of
predicates, and so forth.

The levels of the type hierarchy are different sorts, logically --
they are not necessarily understood as disjoint domains (or as
cumulative) because we cannot even pose the question whether things of
different types are equal or not in the language of type theory.

I regard the intuitive motivation for type theory as unexceptionable;
it is certainly as sound as that for ZFC.

But I also regard type theory as notationally awkward and annoying to
work with.  One of the reasons that it is annoying is that it is
polymorphic in an irritating way.  For example, the natural way to
define the number 3 is as the set of all sets with three elements
(this is not circular because "having three elements" is expressible
in first-order logic without any reference to 3).  But one obtains a
"different" number 3 at each (sufficiently high) type!

Further, the theory of types 1,2,3... is the same as the theory of types
0,1,2..., because our axioms are systematically polymorphic.  (this is 
what Russell called "typical ambiguity" in PM).

The notational inconvenience of the types causes us to desire a one-sorted
theory.  The polymorphism suggests that one might be able to collapse the
types and obtain a notationally and philosophically more appealing scheme.
The collapse we think of is one which (for example) identifies all the
different "numbers 3" of different types.

This is the point at which Quine had arrived when he proposed NF; he
correctly describes the theory which results if one collapses the
types (in extensional type theory) but sidesteps the issue of whether
the collapse can be motivated better than by noting that no contradiction
seems to result (in any event, this formalist motivation was weakened 
seriously by Specker's disproof of AC).

We should practice philosophical introspection at this point.  If we
seriously believe in a type theory, and propose to amend our
type-theoretical view of the world by collapsing the hierarchy of
types, what are we actually doing on a philosophical level?

My answer is that we are proposing a scheme whereby the types are to
be identified (they have not been thought of so far as disjoint
domains but as "incommensurable" domains -- we have made no provision
for deciding when a type 1 and a type 3 object might be the same or
different, and moreover have forbidden ourselves by a linguistic
discipline to even ask the question as to whether they are the same or
different).

A note: this suggests that we might really want to take our type
theory to be nonextensional (or at least, we shouldn't be shocked when
our technical development forces us to make our type theory
nonextensional retroactively!).  By proposing to identify type 1 (sets
or predicates) with type 0 (objects), we are saying that predicates
are objects; but we might not want to believe that all objects are
predicates, so we might find it appealing a priori to adopt a
nonextensional type theory in which type 1 includes all predicates of
type 0 objects (or, equivalently, sets of type 0 objects) and also
includes some other things (among which we might include objects that
we are pretty sure are not predicates in the usual sense).  So type 1
might reasonably be taken to include urelements as well as sets (and
so would each higher type).

When we identify the types, there still remains a formal residue of
type theory in the form of the stratification restrictions on
comprehension.  What do these mean, philosophically?  Why don't we
make the leap to unstratified (and inconsistent!) naive comprehension
as soon as we collapse the type hierarchy?

One can see this by thinking about what the types are really doing,
even in the type theory.  Objects of different types are restricted to
particular contexts; they are used in different ways in the typed
language.  When we collapse the type structure (saying that the
underlying domains of the various types are to be identified) but
persist in defining sets in a "typable" manner, this suggests that we
still regard the types as important, considered not as indicating
different kinds of object, but as indicating different aspects of
objects (different ways that objects can be used).  When we use an
object as a predicate, we are doing something different with it than
when we use it as a type 0 object (an individual).

Though we find it convenient to say that a predicate is (some)
individual, we are still not interested in the question of whether the
object identified with a predicate has that predicate: the statement x
E x is meaningful in our now untyped language (and provable for some
values of x: if V = {x | x = x}, then V E V is true because a E V for
any a).  But this is not a feature of x which interested us when we
were working under type discipline, and it doesn't cramp us that we
are not provided with the set {x | x E x} (or its paradoxical
complement).

Here's the intuitive picture: we live in a universe of objects, all of
the same sort, of which some (the sets) are used to represent
predicates.  Because predicates are objects, some predicates (those
which hold only of objects identified with predicates) also represent
predicates of predicates: we have objects representing predicates,
objects representing predicates of predicates, and so forth.

We regard any given object as having a hierarchy of different aspects
under which it can be viewed; properties of objects which depend on
the relationships between their different aspects (i.e., those which
were not expressible in our typed language) are not guaranteed to be
represented by any object.  So, for example, there may be no object
representing the predicate of self-membership (no set {x | x E x}),
because in self-membership we consider one and the same object qua
individual and qua predicate.

As I commented above that type theory views the types not as disjoint
domains but as "incommensurable" domains, I suggest that in the
picture of sets that we are developing here, relationships between
"incommensurable" aspects of one and the same object are not
accessible to us in defining predicates which have extensions.

Our criterion for deciding what predicates are implemented as objects
(what sets there are, what comprehension axioms hold) can be seen to
be less annoyingly intensional by observing that it is equivalent to
finitely many comprehension axioms, all intuitively fairly appealing
(NF(U) is finitely axiomatizable, and has nicer finite axiomatizations
than the quite ugly one originally proposed by Hailperin; it can be
formalized without any reference to types at all).  But for practical
use of NF(U) one would need to use the finite axiom set to prove
stratified comprehension as a meta-theorem.

The question of whether this is possible is not settled by this
development!  One has to carry out the model theoretical argument of
Jensen to show that it really can be done.  The argument can be
carried out in type theory; upon discovering that the argument only
seems to work in nonextensional type theory, we can observe that the
type theoretical foundations are not compromised by weakening
extensionality.  The argument of Jensen then allows us to abandon
distinctions of type and work in NFU (we can show in type theory that
if type theory is consistent, NFU is consistent).

To regard this move as appealing (even from the type-theoretical
standpoint) we cannot view set theory a priori as a theory of
absolutely arbitrary collections of objects.  If we believe a priori
(even in the framework of type theory!) that type 1 must contain every
collection of type 0 objects, then, while we see that the move to NFU
is technically legitimate, we will regard it as false to our
philosophical motivation for set theory.  But if we view set theory as
a study of the reification of predicates (as a study of "universals",
in philosophical parlance) then the move to NFU described here is not
false to our philosophical motivation, and it is appealing because it
allows the reification of more predicates (in an untyped context) than
the Zermelo approach allows (for example, we reify the predicate of
"being" which holds of everything (we have a universal set)).  If we
belong to the former school of thought, we still have a way to
collapse the type hierarchy which is consistent with our philosophical
view, which will lead us to Mac Lane set theory (and then could
naturally lead on to full ZFC). (I'm not saying that this is how ZFC
developed historically).

This is not as simple as the motivation for ZFC; that's undeniable.
But it is an intelligible viewpoint.  The contrast between a view of
sets as arbitrary collections and a view of sets as implementations of
universals in the previous paragraph might be instructive: an
implementation of universals might be expected to be more complicated!

There is a continuing story here (just as there is a continuing story
leading from Zermelo set theory to ZFC and so on to large cardinals).
There are residual annoyances in NFU (or in NF) which are not
analogous to anything in ZFC.  These can be reduced by adopting
natural simplifying axioms like Rosser's Axiom of Counting or my Axiom
of Small Ordinals alluded to by Simpson above.  These axioms cause
increases in consistency strength (one symptom of this is that they
allow the proof of the existence of "large cardinals" (which need to
be distinguished in this context from "big cardinals" like the
cardinality of the universe (present in any version of NFU) -- there's
a discussion of "bigness" versus "largeness" going on now on the NF
list); for example, the Axiom of Counting allows the proof of the
existence of beth-omega, while the Axiom of Small Ordinals allows one
to prove the existence of inaccessibles, Mahlo cardinals and so forth.
Consistency proofs for NFU with these axioms can be given in ZFC (and
could be given as well in type theory with large cardinal assumptions,
and so can be given in NFU itself plus large cardinal assumptions).

Just as there is a view of NFU from a ZFC standpoint (the theory of
nonstandard initial segments of the cumulative hierarchy with
automorphisms moving a level) so there is a view of Zermelo-style set
theory (not necessarily of ZFC -- this depends on how strong a version
of NFU one is working in) as the theory of isomorphism types of
well-founded extensional relations.  It is amusing (but not surprising
since more work goes into building the NFU view of things) that the
description of the Zermelo world inside the Quine world is technically
simpler than the description of the Quine world inside the Zermelo
world.  It is even more amusing that the initial segment of the
cumulative hierarchy thus pictured inside NFU turns out to have an
external automorphism (definable in NFU but not in the internal
language of the interpreted Zermelo-style theory) which moves a level;
NFU reflects its own model theory (as seen from the Zermelo
standpoint) internally!

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 at math.boisestate.edu
not glimpse the wonders therein. | http://math.boisestate.edu/~holmes