This posting is an advertisement; it also discusses foundations using
NFU at length.

My book "Elementary Set Theory with a Universal Set", an introductory set
theory text using NFU (New Foundations with urelements) instead of ZFC
has appeared.  Information about ordering the book can be obtained from
me (holmes@math.idbsu.edu).

The moderator allowed me to post the ad, but advised me to give it some
fom content; this isn't difficult, since the intended audience is professionals
interested in foundations of mathematics.  The book is ostensibly a text
which could be used at an advanced undergraduate or graduate level to teach
set theory (though it doesn't really have nearly enough exercises) but
one should really teach undergraduates the standard theory everyone else
learns!

I didn't originally intend to write a book at all; I got tired of
making elementary mistakes in set theoretical constructions in NFU (by
false analogies with what one can do in standard set theory), so I sat
down and worked through Halmos's Naive Set Theory, redoing everything
in NFU (this worked in the sense that I stopped making stratification
mistakes!).  What Simpson suggested might have FOM interest is a
discussion of the difficulties one encounters in doing this.

The first difficulty (and the obvious one) is motivating stratified
comprehension.  My feeling is that stratified comprehension, as usually
presented, makes no case for NF(U) as an independent foundation:  one 
really needs to understand the theory of types to see what is happening.

The approach I adopted was to present a finite axiomatization of NFU.
The finite axiomatization which is normally cited (by Hailperin) is
virtually unintelligible.  I developed my own:

(extensionality axioms)

(1) extensionality axiom for sets
(2) atoms (non-sets) have no elements

sets form a Boolean algebra:

(1) the universal set exists
(2) sets have complements
(3) sets have Boolean unions
(4) sets have unions in the usual sense

	[4 is an infinitary version of 3] 

finite structures:

(1) singleton sets exist
(2) defining characteristic of the ordered pair -- pairs are equal
iff corresponding projections are equal
	[I take the pair as primitive]
(3) Cartesian products exist

algebra of relations:

(1) converses of relations exist
(2) relative products (compositions) of relations exist
(3) domains of relations exist
(4) images of sets under the singleton operation exist
(5) the equality relation and the projection relations of the pair exist

	[the assertion that the projection relations of the pair
	exist is actually the Axiom of Infinity!]

The headings correspond to chapters in which the axioms are introduced. 

At this point I stopped and proved a meta-theorem to the effect that
any formula of first-order logic in which all of the predicates or
relations in atomic formulas have set extensions itself defines a set.

>From this, it is easy to prove that \in (membership) does not have a set
as its extension (by appealing to Russell's argument).

Instead, I adopt as the final axiom

(1) the inclusion (subset) relation exists as a set.

I then prove the Scheme of Stratified Comprehension as a meta-theorem.
The axioms to this point are equivalent to NFU + Infinity in strength
(the type-level ordered pair provides an inessential increment of
strength).

This is a concrete example of my proposal that finite axiomatizations
supported by meta-reasoning to schemes are adequate for foundations.
The adequacy of the finite list of axioms (in my opinion) is seen in
the fact that they are intuitively convincing propositions which "hang
together"; I would not have regarded Hailperin's very technical axioms
as adequate for foundational purposes, since they could only be motivated
by the end of obtaining stratified comprehension.

It will be seen below that the full system of the book contains an
infinite axiom scheme!

There follows a chapter in which I discuss philosophy of set theory along
lines similar to things I have posted on this list: I discuss set theory
in general and the reasons for the paradoxes, then present the ADT motivation
for the criterion of stratified comprehension.

The presentation of order and of operations on families of sets which
follows is based on Halmos.  Stratification as a technical issue does
appear in the NFU treatment.  For example, the equivalence classes of
a partition are at a relative type one higher than that of the
elements of the domain being partitioned.  This causes some potential
technical problems (the "map" x |-> [x] sending an element of the
domain to its equivalence class is not a set) but I turned this to
advantage: it makes a natural point at which to introduce the Axiom of
Choice, which enables the choice of a representative from each
equivalence class: the representatives do live at the same type as the
elements of the domain being partitioned, so equivalence class constructions
do work without type problems.

The definitions of Cartesian products and disjoint sums of indexed
families of sets are tricky to get right in the NFU context, and the
former is used as a detailed case study of the use of stratification.

The definition of the natural numbers and treatment of Peano arithmetic
is quite easy, though technically quite different from the usual treatment.
The Frege-Russell definition of the natural numbers is used:  3 is the set
of all sets with three elements.  This is achieved without a hint of 
circularity.

The relation between arithmetic and set theory occasions the introduction of
a new axiom.  Rosser (in his Logic for Mathematicians, which used NF
as the foundation) noted that one cannot prove in NF that {1,...,n} has
n elements.  He introduced this assertion as the "Axiom of Counting",
and we follow him, though we use a different formulation.  The difficulty
with proving the axiom is that "{1,...,n} \in n" is not a stratified
sentence, so does not necessarily define a set, which causes the obvious
induction argument to fail.  Orey showed that the Axiom of Counting is
actually independent of NF if NF is consistent; the proof can be adapted
to NFU, which indeed has models in which the Axiom of Counting is false.
Once Counting is adopted, it is no longer necessary to assign relative
types to variables restricted to the set of natural numbers (or indeed to 
such larger sets as the reals) for purposes of stratification.

The construction of the reals as Dedekind cuts in the rationals is
presented and carried off without incident.

The usual equivalent forms of the Axiom of Choice are presented and
shown to be equivalent to AC in ways not essentially different from
the ZFC approach.  AC is shown to be equivalent to Zorn's Lemma and to
the theorem "the universe can be well-ordered".

The ordinal numbers are defined as equivalence classes of
well-orderings under similarity.  The transfinite recursion theorem is
proved, and the usual operations on ordinals are defined.  It is
proved that the natural order on the ordinals is a well-ordering.

The fun begins at this point, where the surprising resolution of the
Burali- Forti paradox is presented: one cannot prove that the
restriction of the natural order on the ordinals to the set seg(alpha)
of ordinals less than alpha is alpha, because seg(a) is two types
higher than alpha.  One then discovers that this is fortunate: if
Omega is the order type of the ordinals, the order type of the natural
order on seg(Omega) is (much) less than Omega.

The first of a number of "T operations" are introduced: if the order
type of a well-ordering R is alpha, the order type of the order
induced by R on singletons of elements of the domain of R (notice that
this relation is one type higher) is T(alpha); the order type of the
natural order on seg(alpha) can be proved equal to T^2(alpha).  T is
an external endomorphism of the ordinals (it is not a set function but
a proper class map); the descending sequence of ordinals T^i(Omega) is
an (externally countable!) proper class.  (This is an internal "hint"
as to what models of NFU look like).

Ordinals fixed by the T operation are called "Cantorian" ordinals
(for reasons which will be revealed below).  Cantorian ordinals are
small relative to Omega, and may be thought of as the "familiar"
ordinals of the usual set theory.  The Cantorian ordinals do not make
up a set; if they did, the Burali-Forti argument could be reproduced.

I then introduce an extremely strong axiom scheme, which makes the full
system of the book considerably stronger than ZFC.

Define a "small" ordinal as an ordinal less than some Cantorian ordinal.

The Axiom of Small Ordinals:  For each formula \phi, there is a set
whose small ordinal elements are exactly the small ordinals such
that \phi.

Solovay has shown recently that the strength of the system NFU +
Infinity + Choice + Small Ordinals is the same as that of ZFC - Power
Set + "there is a weakly compact cardinal" (this result is not cited
in the book, but there is some discussion of the considerable strength
of the system); a further axiom later in the book gives it even more
strength.

Immediate consequences of the Axiom of Small Ordinals include Counting
(which is redundant after this point), Mathematical Induction for all
unstratified formulas (which doesn't affect the arithmetic of NFU directly
but has very strong consequences in set theory) and transfinite induction
on the Cantorian ordinals for unstratified formulas.

The book then turns to the development of the theory of cardinal
number.  Cardinals are defined as equivalence classes of sets under
the relation of being the same size, defined in the familiar way.
Addition and multiplication of infinite cardinals are shown to have
the familiar properties we expect in much the same way as in the usual
set theory.

Exponentiation presents a different picture.  The usual way of
defining exponentiation of cardinals is not stratified.  This is
corrected by introducing a T operation on cardinals (T(|A|) is the
cardinality of the image of A under the singleton operation); 2^|A|
is defined as T^{-1}[|P(A)|] (the T^{-1} operation is not always defined;
the exponential function is partial.  General exponentiation A^B is defined
similarly.

The Cantor theorem does not take the form |A| < |P(A)| in NFU; it
takes the form |P_1(A)| < |P(A)| which it takes in type theory, where
P_1(A) is the set of one-element subsets of A (this is equivalent to
kappa < 2^kappa under the stratified definition of exponentiation).
The Cantor paradox |V| < |P(V)| <= |V| is avoided: instead we have
|P_1(V)| < |P(V)| <= |V|.  Note that P(V), the set of sets, is not
necessarily the same as V, the universe.

We prove K\"onig's Theorem, which is a considerable technical effort in
stratification, due to the role of infinite products and sums of indexed
families of cardinals.

Specker's theorem that NF |= ~AC is proved, but in the form NFU + AC
|= "there are atoms".  It is shown that |P(V)| is _much_ smaller than
|V|.  A trivial corollary is that there cannot be a set-theoretical
definition of the primitive type-level ordered pair.

The notion "Cantorian" is explored further.  A set A is said to be
Cantorian if it is of the same size as P_1(A) (so that the familiar
form of Cantor's theorem holds); the Cantorian ordinals defined above
turn out to be exactly the order types of well-orderings of Cantorian sets.
A set is said to be "strongly Cantorian" if the restriction of the
singleton map to the set exists as a set function.  Clearly a strongly
Cantorian set is Cantorian.  The Axiom of Small Ordinals implies that
all Cantorian sets are strongly Cantorian.

Solovay has shown recently that the strength of NFU + Infinity + Choice
+ "all Cantorian sets are strongly Cantorian" (notice that Small
Ordinals is _not_ part of this theory) is precisely the same as the
strength of ZFC + the scheme asserting the existence of an n-Mahlo for
each concrete n.  This result is cited but not proved in the book.

The book presents ZFC in two different ways.  A coding of set theory
into the ordinals is used and it is shown that the Cantorian ordinals
provide an interpretation of ZFC.  The proofs require the Axiom of
Small Ordinals.

The book then presents a development of a Zermelo-style set theory in
the isomorphism classes of well-founded extensional relations.  Once
again, Small Ordinals is used to show that ZFC is interpretable in the
Cantorian isomorphism classes.

The surreal numbers of Conway are presented; like the ordinals, they cannot
be presented in the same way in NFU that they are in ZFC.

Basic concepts of transfinite cardinal arithmetic are presented, and 
the theorem of Solovay that there is an inaccessible cardinal is proved.
(This provides a set model of ZFC in the isomorphism classes of well-
founded extensional relations).  This proof can be refined to demonstrate
the existence of n-Mahlos for each n, but the refinement is not presented
in the book.

A final axiom is presented (for each non-Cantorian ordinal alpha, there
is a natural number n such that T^n(Omega) < alpha) which causes the
strength of the theory to become precisely that of Kelley-Morse set theory
with a predicate providing a kappa-complete ultrafilter on kappa, where
kappa is the proper class ordinal.  The proof of this in one direction
is outlined on an informal level in the book.

The last chapter discusses stratified lambda-calculus, giving an alternative
axiomatization of the entire book along the lines suggested in my Ph.D.
thesis on systems of combinatory logic equivalent to NF and NFU.

My conclusions from all this: it is certainly possible to use NFU as
an independent foundational approach.  The technicalities of
stratification do require some getting used to.  The gain (if any)
lies in the availability of intuitively appealing "large" collections
(though they don't have all the properties one expects) and in the
fact that natural extensions of NFU seem to give considerable
additional consistency strength.  The real advantage, since I do _not_
actually advocate a change of foundations from ZFC to NFU, is the
availability for comparison with ZFC of a fully developed alternative
approach to foundations with a quite different resolution of the
"paradoxes", which affords a better understanding of what is really
happening there.  I suppose that it is possible that study of the
"boost" in strength in extensions of NFU might be useful in the study
of some large cardinal hypotheses (I'm not making a claim here, only
a suggestion).

Certain very important foundational tools (constructibility and
forcing) can be obtained in NFU only by implementing them in the
isomorphism classes of well-founded extensional relations (effectively
by reproducing the ZFC approach); this is not surprising, because both
of these methods take essential advantage of the construction of the
world of ZFC via a cumulative hierarchy.  But it appears from looking
at the NFU construction of a Zermelo-like set theory that NFU has a
pretty good internal picture of the cumulative hierarchy itself,
modified by the presence of an external endomorphism pressing a high
(nonstandard) level of the hierarchy downward.  NFU has a natural
internal picture of the way that set models of NFU must be constructed
in ZFC (or in NFU itself), which is philosophically interesting.

The book does not discuss the model theory of NFU in ZFC (this being
beyond the ostensibly elementary level of the treatment); a reference
for this and much else is Thomas Forster, {\em Set Theory with a
Universal Set\/}, Oxford logic guides no. 20 or 31 (2nd ed.)  Also,
Jensen's original paper in Synthese 19 or my paper in Modern Logic,
vol. 4, no. 1 would give this.

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