FOM: NFU as foundations?

[Randall Holmes]

A note to summarize my interests in NFU as a foundation for mathematics:

I have made it a project to explore the possibility of using
extensions of NFU (the version of Quine's New Foundations, due to
Jensen, in which urelements are permitted) as the foundation for
mathematics.

See my book "Elementary Set Theory with a Universal Set", ISBN
2-87209-488-1, for details (ordering details and errata slip available
from my web page).  This appears on the surface to be an elementary
set theory textbook using an extension of NFU instead of ZFC.

As a first-order formal theory, extensions of NFU work as a foundation
for mathematics.  It has some advantages and some disadvantages.  It
is in fact not terribly different from the standard approach (one can
learn to translate fairly readily between a ZFC-based viewpoint and an
NFU-based viewpoint.  I can testify that it is possible to learn to
think in terms of NFU foundations.

As soon as one takes a second-order view of things (or, from other
standpoints, as soon as one starts to apply certain natural
metatheoretical considerations) ZFC wins hands-down.  The difficulty
is that the comprehension scheme of NFU gives a special role to
certain properties on "intensional" grounds (they can be motivated on
better than "purely syntactical" gounds) which are quite hard (though
not impossible) to motivate.  It should be noted that another
interesting alternative set theory, much more closely related to ZFC,
the set theory of Ackermann, has similar difficulties.

I would have to say that my working foundations are really in ZFC,
since I rely on Jensen's consistency proofs in ZFC for my intuition
about the "safety" of NFU foundations, and rely on stronger extensions
of ZFC for proofs of consistency of stronger extensions of NFU.  I
think that it is intellectually possible to motivate NFU in a way
which does not involve ZFC at all (via the simple theory of types) but
that's not my actual approach.  So I am not really a heretic :-)

But I think that it is a valuable exercise to consider alternative
foundations.  It is useful to see that they are possible, and seeing
alternative approaches helps one to see what foundations do for us.
The systems I am most interested in are NFU and extensions (NF and its
other known-to-be-consistent subsystems are too eccentric), the set
theory of Ackermann and some systems related to "nonstandard analysis"
(the alternative set theory of Vopenka, which is quite weak, and the
set theory IST).  This is not intended as an exhaustive list.

Familiarity with NFU can help one to avoid making silly assertions
such as the frequently made assertion that the universal set is an
inconsistent totality; NFU + Infinity + Choice is a set theory
adequate for most of classical mathematics in which there is a
universal set, and it is consistent iff the simple theory of types is
consistent (and so certainly consistent if ZFC is consistent).

My theorem proving work uses stratified lambda-calculus (NFU adapted
to a theory of functions rather than sets) as its "higher-order
logic".  This works out fairly well, once support is built in for
technicalities involving "strongly Cantorian sets".  Graduate students
in computer science learn to use this higher-order logic without too
much difficulty (I motivate it as a polymorphic version of type
theory).  (I am not claiming that anyone has used it to prove very
profound results!).

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