Date: Mon, 29 Mar 1999 12:17:01 -0700
From: Randall Holmes <holmes@catseye.idbsu.edu>
Subject: FOM: foundations in NFU

In my previous post re NFU as foundations I feel that I may have been
"letting down the side" from the standpoint of fellow NF-istes (there
is at least one on this list other than myself).  So I will address myself
in this note to the advantages of NFU as foundations and the possibility
of adopting NFU and extensions as the foundation of mathematics on
autonomous grounds.

The obvious advantage of NFU is that one retains "big" objects like
the universal set and the ability to use many definitions proposed by
Frege and Russell.  The universe of sets is a Boolean algebra.  One
can define cardinals as equivalence classes of sets under the usual
notion of "being the same size" (this subsumes Frege's definition of
the natural numbers as a special case) and ordinals as equivalence
classes of well-orderings under similarity.  These definitions
certainly have an intuitive character, and it is instructive to see
that they do not necessarily lead to paradox.  (I'm not claiming that
they are the "best" definitions).

The stratification criterion of NFU (which is the same as the
stratification criterion for NF) is the only criterion for
comprehension known which allows a universal set (as opposed to a
universal class) and allows the fluent expression of mathematical
concepts and reasoning.  A frequent criticism of NF is that its
comprehension criterion is only a "syntactical trick" adopted merely
because it avoided the known paradoxes.  This is historically correct;
but it does not rule out the adoption of the stratification criterion
for comprehension on other grounds.

There is an intuitive motivation for the stratification criterion; it
is not nearly as convincing as the intuitive picture which convinces
most of us that ZFC is consistent, but it can motivate an inquiry into
the consequences of NFU on a better basis than the one supplied by
Quine.  It is supported by mathematical results in two directions:
there is a theorem of Forster which formalizes the intuitive
motivation for the stratification criterion, and there is the Jensen
proof of the consistency of NFU, which supplies us with the
preliminary picture of the intended interpretation of NFU as an
autonomous foundation.  The progression of stronger theories in the
strong axioms of infinity paper allows one to see how considerations
internal to NFU itself allow one to get a clearer and clearer picture
of what the intended interpretation for NFU as a foundational theory
is.  I admit (I emphasize) that this intended interpretation is less
easy to understand at the outset than the intended interpretation of
ZFC.

The "intuitive motivation" is as follows.  Consider a class of objects
to which we have not assigned any structure.  We convert this into a
set theory by associating classes with objects to produce sets (things
which can both have elements and themselves be elements).  Consider
the following proposed extension for a set (it is not paradoxical!):
"the set of all sets which are elements of themselves".  We choose an
object Delta to represent this extension.  For each object x, we will
put x in the extension associated with Delta just if we put x in the
extension associated with x.  When we arrive at the question of
whether Delta should be put into the extension associated with Delta,
we ask whether Delta has been put into the extension associated with
Delta -- we are at an impasse!  (The impasse is not quite as bad as it
would be if we were considering the complement of Delta, of course :-)
My claim is that there is something obviously wrong with the
"specification" of the purported set Delta.  Our objects has no
distinguishing characteristics at the outset; it is a matter of
arbitrary choice which "bare object" is associated with which
extension (class of bare objects).  But the question of whether any
given x belongs to Delta is defined in terms of the correlation
between x and its extension.  Consider the construction of our set
theory as the implementation of the abstract data type "class"; the
only thing which should matter about a class is its elements.  The
question as to whether x belongs to the class associated with x is not
a legitimate question about the class implemented by x (or indeed
about the bare object x) because it relies, as it were, on details of
the implementation of the data type "class"; a nonempty class A with
nonempty complement could be associated either with an object
belonging to A or an object not belonging to A, which has nothing to
do with any properties of A itself, but only with irrelevant details
of the implementation of classes as sets.

One goes on to observe that "class" is not the only type implemented
by the association of extensions with each object; one has also
implemented "class of classes", "class of classes of classes", and so
forth.  There is a hierarchy of sorts of object (familiar from type
theory) each of which is interpretable in this context.  The
correlation between the identities of one and the same object
considered in different "roles" is dependent on arbitrary features of
the implementation (the original correlation of objects with
extensions) and the specifications of sets in the theory should not
rely on thsese arbitrary identifications (the security of the abstract
data type implementations should be respected).  This gives an a
priori reason (not depending on awareness of any paradoxes!) to accept
as specifications of sets only formulas in which any given object is
mentioned in only one role.  But this is exactly the criterion of
stratified comprehension!


Another way to put this is that since the correlation of objects with
extensions is arbitrary, a redefinition of the membership relation by
permuting the extensions assigned to objects should have no effect on
what classes of classes, classes of classes of classes, and so forth
are realized (obviously the classes realized are not affected).
Forster has proved that the formulas in the language of set theory
which are invariant under permutations which preserve the classes of
higher-type objects which are implemented are exactly the stratified
formulas (though he proved this in a context where full extensionality
holds, it ought to adapt to a context with urelements as long as the
permutations do not send sets to urelements or vice versa).

This provides a genuine motivation for rejecting unstratified
instances of the comprehension schema which can be motivated prior to
the observation that some of these are inconsistent.  It does not
constitute a knockdown argument that the collection of stratified
comprehension axioms is consistent (that the axioms really describe a
possible set theory); this is provided by Jensen's proof.  But it does
provide a genuine reason to be interested in the stratification
criterion for comprehension.

A point which should be made is that the stratified comprehension
scheme can be replaced by a finite set of comprehension axioms which
are intuitively appealing.  This helps to dispel the objection that
stratified comprehension is a "syntactical trick", but it does not
dispel the problem of identifying a structure which actually satisfies
these comprehension axioms.

Notice that nothing in the construction suggests that every object
should be assigned an extension; urelements make perfectly good sense
in this scheme.

The Jensen proof (and variants) give us a picture of what a model of
NFU can be thought to be like.  NFU can be viewed (by one who relies
on ZFC foundations) as a notational variant on the theory of models of
a fragment of Zermelo set theory with a nontrival external
automorphism moving an ordinal.  The domain of the model of NFU is a
V_alpha with alpha>j(alpha) [j being the automorphism] and the
membership relation x \in y of NFU translates to "j(x) \in y and y \in
V_{j(alpha)+1}.  Notice that information about the members (in the
Zermelo sense) of urelements is discarded.

There are a couple of objections which can be raised to the
urelements.  The first is that we ought to be able to get a version of
NFU with pure sets only (this would be NF).  This is based on a false
analogy with the relation between ZFA and ZFC.  One cannot carry out
inductive arguments or recursive constructions on membership in NFU.
The stratification criterion for comprehension excludes this formally
and the intuitive motivation for stratification also excludes it;
induction or recursion on the membership relation will certainly
depend strongly on details of how classes of objects are correlated
with objects to implement our set theory (the axiom of foundation, for
example, is easily perturbed by redefinitions of membership using
permutations).  The predicate "is a pure set" cannot be expected to be
definable in NFU, and can be rejected as involving violations of "data
type security".

Though it is not possible to carry out a complete extensional collapse
and obtain a model of NF from a model of NFU, it is interesting to
note that it _is_ possible to carry out a "weak extensional collapse"
which converts a model of the stratified comprehension axioms not
satisfying any extensionality axiom to a model of NFU!  (this is a
construction due to Marcel Crabb\'e).

A subtler objection is that we ought to be able to confine our
attention to structures of mathematical interest; one therefore
objects to a foundational theory which requires structureless
urelements.  It is possible to correct this (to get an interpretation
of NFU and retain information about the structure of the urelements)
in a natural way inside NFU itself.  If one investigates the theory of
well-founded extensional relations "with top" (pictures of the
membership relation on transitive closures of sets of a Zermelo-like
theory) one finds an interpretation in NFU of a fragment of Zermelo
with a nontrivial external automorphism, which can be converted to an
interpretation of NFU in the standard way; in this interpretation it
is clear from the standpoint of the ambient NFU that the "urelements"
have interesting structure, and one can add predicates to the
interpreted NFU which allow one access to this structure.  But I don't
myself see the force of the objection; I don't think that ZFA is any
less a foundation for mathematics than ZFC.

As with ZFC, whose underlying intuitive picture motivates further
extensions by large cardinal axioms, experience with NFU and a notion
of what the "intended interpretation" should be like motivates a
sequence of extensions to stronger and stronger theories.  These
extensions are generally motivated by a desire for control over the
behaviour of the underlying external automorphism (whose restriction
to such structures as the ordinals, cardinals, or isomorphism classes
of well-founded extensional relations with top is definable (as a
proper class, not a set) in NFU, though the entire automorphism is
not); natural assumptions about the automorphism lead to extensions of
NFU which can be shown to be consistent if one appeals to large
cardinal axioms (of intermediate strength) in ZFC.

The strongest extension of NFU which I have considered (NFUM in my
strong axioms of infinity paper, accessible from my web page) is (part
of) the theory of a particular structure of considerable mathematical
interest: it is related to a (necessarily non-well-founded) model of
ZFC with an automorphism obtained in a natural way from the elementary
embedding of the universe into itself associated with a measurable
cardinal.  The theory NFUM, originally motivated by considerations
internal to NFU itself, captures a large part of the theory of this
structure (it is equiconsistent with Kelley-Morse + a predicate on
proper classes which is a kappa complete measure on the proper class
ordinal kappa, and the proof of this equiconsistency involves 
reconstructing the analogue of the model of ZFC alluded above in this
theory; this is harder because the measurable is a proper class
ordinal, so we can't look past it).

When I do foundational work in extensions of NFU, I am not playing a
formal game; I have definite structures of mathematical interest in
mind, which can also be described in (extensions of) ZFC.  There is
historical interest in the elementary constructions used in NFU
foundations, because they are similar to the constructions which
Russell and Frege intended to use -- and NFU foundations demonstrate
that it is possible to use those definitions without paradox.  There
is some interest in seeing how considerations native to NFU motivate
extensions of NFU of surprisingly high consistency strength,
culminating in NFUM, which is just short of a measurable cardinal in
strength.

I reiterate that there are weaknesses of an approach to foundations
based on NFU.  Real confidence in the consistency of NFU + Infinity
needs to be based on the prior conviction that Zermelo set theory or
the theory of types with infinity is consistent (so that Jensen's
proof or a variant can be carried out).  This is not fatal to a claim
that NFU is an independent approach, because it _can_ be viewed as a
revision and strengthening of the theory of types.  But I imagine that
(as in my case) an appeal to the intuition behind ZFC foundations is
what would really be at work for most of us.  There are technical
reasons why working in NFU can be less pleasant than working in
Zermelo-style set theory in some contexts (having to do with the
explicit appearance of unfamiliar operations on ordinals, cardinals,
and other isomorphism classes of structures which represent
applications of the underlying automorphism).  The structures which
realize the "intended interpretation" of ZFC are simpler than those
which realize the intended interpretation of (strong extensions of)
NFU.  The "intensional" character of the comprehension scheme of NFU is
problematic, though it can be replaced by a finite list of intuitively
appealing special cases (see my book for one way to do this).  The
advantage overall goes to ZFC; I don't dispute that.  But foundations
in NFU, just as adequate in principle and actually usable in practice
(though admittedly not as good as ZFC), can be justified.

One-word dismissals are _not_ in order.  It seems to be very important
to Friedman that we all acknowledge the importance of ZFC; I, for one,
do acknowledge that ZFC is important.  But the degree of importance
that he attaches to the exact theory "first-order ZFC" is impossible
to justify.  There are mathematicians who do not accept the validity
of this theory (or even of classical first-order logic!)  There are
communities of mathematicians who tacitly accept less than full ZFC
(theoretical computer scientists who work with type theories, for
example, but most of mathematics outside set theory needs a great deal
less than ZFC) and communities of mathematicians who tacitly accept
more than ZFC (I have in mind those who work with very large
cardinals, but I think that a majority of set theorists might regard
"the first inaccessible cardinal" as a mathematical object which they
can talk about with some confidence).  There are explicit proposals on
the table for foundations of mathematics which have some following and
are not precisely the same as ZFC: I have in mind Kelley-Morse set
theory (stronger) and Mac Lane set theory (bounded Zermelo set theory
- -- weaker) (not NFU, which has no substantial following, as I am very
well aware!).

I do not promote NFU as an alternative foundation for mathematics in
the sense that I think that anyone should stop using the (better) ZFC
foundations and switch to NFU foundations.  I think that those who are
interested in examining the foundations should be familiar with
alternatives.  An alternative foundation may be useful for some
particular purpose (for which it need not be understood as "the"
foundation; an interpretation in terms of another foundational scheme
can be provided).  Independently of the practical merits or demerits
of particular schemes, acquaintance with alternative foundations can
help one to see what foundations do for us (and what they can't do, as
well).

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

Date: Tue, 30 Mar 1999 12:04:12 -0700
From: holmes@catseye.idbsu.edu
Subject: FOM: a correction

This is  a clarification of part of my last posting on
foundations in NFU.  The description of the intuitive motivation of
stratification is something I have written down many times, and this
time I was too elliptical.  I didn't explain the use of the word "role"
which I use in this account.

I'll recapitulate and (I hope) make it clear what I meant (perhaps
it is clear anyway).  One supposes that in defining a set theory one
starts with a class of "bare objects" with whose structure one is not
concerned.  One then assigns to (some of) the objects in this class
extensions (which are classes of objects).  (Note that in this picture
it is quite easy to postulate a universal set).

This may be regarded as an implementation of the abstract data type
"class".  Certain objects are now used to represent classes.  Implicitly,
one has also implemented "class of classes", "class of classes of classes",
and so forth.

The set definition "the set of all x such that x \in x" (which is not
paradoxical; there are set theories in which this set exists) can be
criticised on the grounds that the implementation of the abstract data
type "class" is being abused:  which bare object x belongs to a particular
class A of bare objects is not a property of A; for the assignment of
extensions to bare objects might make A belong to itself or not (unless
A = V or A = \emptyset).

Here is where I should have explained my use of the word "role".  In the
sentence "x \in x", the first x can be understood as referring to x as
a bare object, and the second as referring to the class associated with
x.  The problem with the specification is that it depends on the correlation
between x and the class assigned to it, and this is not actually a property
either of x or of the extension associated with it.  In more complex
sentences, the roles assigned to variables will include not only
"bare object" and "class", but also "class of classes" and so forth.
The criterion of security for this hierarchy of abstract data types
 (corresponding to the familiar type hierarchy of the Theory of Types) is
equivalent to the stratification criterion for NFU.  The motivation is 
that the assignment of two different roles to the same variable in the 
specification of a set involves an illicit appeal to the arbitrary assignment of extensions to bare objects (to irrelevant details of the implementation
of classes, classes of classes, etc.), rather than to the properties of 
the classes, classes of classes, etc. which are being implemented.  
The assignment of
roles corresponds to the assignment of types for purposes of stratification;
but here it  may be clearer how the assignment of types can be a 
sensible maneuver
in a theory which is actually one-sorted.

Sorry about the odd format; I am using an unaccustomed text editor.

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