FOM: Insall's questions re NF

[holmes@catseye.idbsu.edu]

Matt Insall said:

Several years ago, I read several books on different set theories.  Quine's
 NF was mentioned, and I seem to recall that in at least one reference, it
 was claimed that NF is inconsistent.  I have been unable to find such a
 reference lately, but in the text ``Foundations of Set Theory'' by
Fraenkel,
 Bar-Hillel and Levy, the following facts are mentioned:
 1.  Quine's system presented in his ``Mathematical Logic'', called ``ML'',
 was shown to be inconsistent by Rosser in 1942, because it implied the
 Burali-Forti Paradox.  (Fraenkel, Bar-Hillel and Levy, footnote on page
168)

I reply:  It is the system of the first edition of Quine's Mathematical Logic
(ML) which was shown to be inconsistent.  It is known that the system of
the second edition of ML is consistent if NF is consistent.  ML extends NF
with proper classes, and in the first edition Quine was too daring in his
approach.

 2.  NF contradicts certain ``simple and obvious facts of classical set
 theory'' (Fraenkel, Bar-Hillel and Levy, page 163, line 2):
     a)  In NF, some sets X are such that if Y = {{x}|x \in X}, then X and Y
 are not equinumerous.
     b)  In NF, some sets X are such that X is equinumerous with the power
 set of X.

I reply:  Guilty as charged.  For b, the universe is an obvious example.
In NFU, the situation is different but not better; the cardinality of the
universe is much _greater_ than that of its power set in NFU + Choice.
Re a, it is an essential feature of "big" sets in NF or NFU that they
are larger than their images under the singleton operation.

Insall continues (edited):

 [...]  In a technical (or formalistic)
 sense, these objections may be ``mere linguistic problems'' (and my gut
 reaction is to say they are just that), but that is quite an unsatisfying
 answer, in my opinion.  The fact that one must always be careful which kind
 of set one is working with in NF in order to use such fundamental intuitive
 notions as the equinumerosity of a set with its set of singletons would
 automatically cause me to prefer ZF, or, even better, NBG.

I reply:

They are indeed basically linguistic problems.  If you did serious work
in a Quine-style system, you would develop somewhat different intuition;
the singleton operation would be recognized as a type-raising operation,
and one would expect it to behave differently.

Insall continues (edited):

[...]
 Steve asked whether NF (or some suitably related system) can be interpreted
 in ZF (or some extension, such as NBG), or vice versa.  Apparently, this
was
 asked also years ago, for the similar questions appear on page 166 of
 ``Foundations of Set Theory''.  I guess this hasn't been answered yet?  Who
 might be working on this?

I reply:

The question of the consistency of NF remains open; no one has any
idea how to model NF.  NF has the bizarre feature that it disproves
AC.  The problem of consistency of NF is extremely hard, and I think
it is correct to say that no progress whatsoever has been made on it,
except for the consistency proofs for fragments (Jensen, 1969;
Grishin, 1969; Crabb\'e, 1983) which really do not suggest what a
model of NF proper might look like.  My paper on "tangled type theory"
might be regarded as making some kind of progress, but I'm not
convinced of this.  (for references, see the bibliography on the NF
home page, accessible from mine).

NFU (NF with extensionality weakened to allow urelements) is known to
be consistent and has a very well understood model theory.  It is,
moreover, consistent with choice.  It has the same axiom of
comprehension as NF -- the problem with NF is not stratified
comprehension, big sets like the universe, sets of singletons
differing in size from their unions, etc, because all of these
phenomena occur in NFU.  (see for a start the article of Jensen in
Synthese, vol. 19).

(It should be noted re point b above that a set which was exactly the
same size as its power set in a model of NFU would be of enormous
interest, since it would allow construction of a model of NF).

There are some other fragments of NF which are known to be consistent. They
are extensional but have restrictions on comprehension, and are less
mathematically fluent than NF (which is in turn less mathematically fluent
than NFU, in my opinion, because of the absence of choice).

Another problem with NF is that there is almost no technology for
relative consistency and independence proofs.  We know, for example,
that NF proves that the universe cannot be well-ordered, but I at
least would be very very very surprised if NF were consistent and proved
that the continuum could not be well-ordered.  But even on the assumption
that NF is consistent, I cannot prove the consistency of NF +
"the continuum is well-ordered", and neither can anyone else.

There are permutation methods, with which very clever things can be
done, but it is known that no assertion expressible in the language of
type theory can be touched by these methods.  There are
metamathematical techniques: Rosser's axiom of counting (the assertion
that any finite set is the same size as its image under the singleton
operation) is known to essentially strengthen NF because NF + Counting
proves Con(NF).

The situation for NFU is entirely different; it supports basically the
same technology for relative consistency and independence proofs that
standard set theory (ZFC) supports (plus the techniques that work in
NF!).  For example, one can do forcing in NFU.  (Actually, one can do
forcing in NF as well, but the forcing construction creates
urelements, so one cannot build models of NF with desired properties
-- one can prove consistency of extensions of NFU in NF using forcing,
which is not what one really wants).

My take on this is that the question of the workability of Quine's
approach was settled in the affirmative by Jensen's 1969 result that
NFU + Infinity is consistent, combined with Rosser's 1953 development
of the foundations of mathematics in NF (which is readily adapted to
NFU).  The question of the consistency of NF is a nasty technical
question (of considerable interest, but merely a technical question);
in my opinion, the question as to whether one should do mathematics in
NF was settled negatively by Specker's 1953 disproof of Choice in NF.
If one is to do mathematics in the style Quine suggests, one should
work in extensions of NFU + Infinity + Choice.  This is merely my
opinion; Forster, for example, would disagree (he does not like
urelements, nor is he nearly as fond of choice as I am, so he ought to
be less enthusiastic about Jensen's result and less discouraged by
Specker's than I am).

I should always note that I do not advocate the abandonment of the
perfectly satisfactory ZFC foundations now in use (an excellent
implementation of Cantor's paradise from which we will not be driven)
in favor of foundations in NFU; but I maintain firmly that alternative
foundational schemes are possible and interesting, and that NFU is one
of the more interesting ones available (and not even very remote from
ZFC foundations!)

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