[FOM] Tolerance Principle (re assertions made about Con(NF))

[Randall Holmes]

Dear fellow FOMers,

I find the conjectures about the consistency question for NF made by Gordeev
to be quite dubious.

All mathematical applications of NF (including everything in Rosser's
book) can be carried out in NFU + Infinity (or better yet, NFU +
"there is a type-level ordered pair" + Choice, which is essentially as
strong).  NFU + Infinity (or the other theory I describe) is just as
strong as the simple theory of types or bounded Zermelo set theory.
(Actually, the axiom of counting that Rosser introduces in his book
increases the strength of a version adapted to NFU to something more
than bounded Zermelo but still much less than ZFC).

The only feature distinguishing NF from NFU + Infinity + Choice is a
disability: it disproves Choice, and not in a way which displays any
consistency strength.

There is _nothing_ to indicate that NF is any stronger than the simple
theory of types with the Axiom of Infinity (that is, bounded Zermelo
set theory), and my conjecture is that that is its strength -- unless
it is inconsistent, which also seems quite possible to me.

Gordeev observes correctly that NF is finitely axiomatizable (all NF
sets can be built using a finite menu of operations).  He is correct
that if we slightly tweaked the definition of the operations (so that
they respect coextensionality) then require that all objects are
actually constructed using the operations, we would obtain NF (extensionality
would follow from the closure conditions, and this would remove the weakening
effect of the modified definitions of the operations).

This is a common approach that naive people who think that the NF
problem must be easy often take (they try to build term models).  [I
am not saying that Gordeev is being naive in this way; I don't think
that he is.]

But I believe that there is no reason whatever to think that the resulting
theory is consistent.  I do not believe that anyone knows how to construct a
model of simple type theory with this kind of closure property, in fact.

There are good reasons to think that the existence of such a model of
NF is a strong assumption, but I don't think the level of strength
approaches that of ZFC (if it is even possible); I would suspect this
of being at the level of strength of "There is an omega-model of type
theory" (if it is possible at all).  The suggestion that this theory
would not be interpretable in ZF or ZF with large cardinals is based
on a false analogy.  The closure assumption in the version of NF that
Gordeev describes does not say that the universe is small in
cardinality, since some of the operations on which the induction is to
be carried out are not set functions.  It does seem to imply that the
universe is externally countable, but it is well-known that this
assumption has no consistency strength to speak of.  I am not saying
that his closure principle does not have strong consequences (it
does!) but that it does not in fact say that the universe is small in
any sense that is visible internally.  In general, there is no true
analogy between the "universe" of NF and the "universe" of ZFC; this
can be seen clearly in the model theory of NFU, where the size of the
universe does not have to have any large cardinal properties (even
when large cardinals are actually present).  In NF the cardinality of
the universe is constrained to have some special properties not
required in NFU (having to do with the way choice fails), but it is
not clear that they are large cardinal properties, either.

So, I ask everyone on the list: _does_ anyone know how to construct a
model of simple type theory in which every element is a term {x |
phi}, where phi is a formula built using logical connectives and
quantifiers, equality, membership, and set abstraction alone (one also
needs constants for type 0 objects)?  Of course one can build such a
model if one has some additional predicates to work with (such as a
well-ordering of type 0); and I do require that type 0 be infinite (if
type 0 is finite it is also easy to see how to build such a model).
This has some bearing on whether Gordeev's program makes any sense,
since a model of the version of NF he proposes would be a model of
simple type theory of this kind (with all types identified), or at
least would be much like such a model.

--Randall Holmes