[FOM] Gordeev on NF consistency -- a clarification

[Randall Holmes]

Dear FOM'ers,

I have received a private communication which suggests that I ought to
clarify something that Gordeev said (and I agreed with) which might be
misunderstood.

Stratified comprehension is equivalent to a finite set of its
instances: this is well-known.  So there is a finite collection of
constructions with the property that if the universe is closed under
these constructions, then stratified comprehension must hold.

Further, Gordeev observed (correctly) that if we modify the definition
of each of these constructions (which will have the shape {x |
phi(x,y_1,...y_n)} to the weaker form {x | (\exists z. z has the same
elements as x and phi(z,y_1,...,y_n)} and then further stipulate that
every object in the universe is actually of one of these forms, then
we obtain extensionality and so the weaker forms of the constructions
are equivalent to the original forms.  (In this context, equality x=y
is understood to be equivalent to (\forall z.x \in z iff y \in z); if
every set is of one of the forms described above, then all sets
respect coextensionality and coextensional sets are thus equal).  So
if there is a model closed under the set of weakened operations which
contains nothing not constructed using one of the weakened operations,
it is a model of extensionality, so is closed under the operations in
their original form, so is also a model of stratified comprehension,
and so is a model of NF.

The claim which is not being made, either by me or (I think) by
Gordeev, is that there is any hope of constructing models of NF by
some kind of iterated closure under the finite set of operations.  For
one thing, the formulas phi(x,y_1,...y_n) involved in the definitions
of these operations involve quantifiers over the whole universe of the
set theory (they are not absolute), so there isn't any possibility of
an iterative construction of the NF universe using these operations
(one needs access to the entire universe as a completed structure in
order to understand the operations!)  There is no analogy with the
(absolute!) G\"odel operations and their role in the construction of
L, for example.  The private communication made me think that both of
us might be incorrectly understood to be making a claim of this kind.

The objection which I was expressing is that for exactly this reason
there is no particular reason to believe that (even if NF is
consistent) there would be any models of this kind.  The intuition
that there are any such models would seem to me to rest on the clearly
invalid informal intuition that some kind of closure under these
operations makes sense.

All of this is related to a notion of "term model" of a set theory
favored by Thomas Forster.  Suppose that our language contains set
abstraction {x|phi} as a primitive.  Then we can reasonably ask
whether there are models of our theory which consist _exactly_ of the
closed terms {x|phi} in which each abstract that appears is an
instance of our comprehension axioms.  I have referred to such
structures as "Forster term models".  If our comprehension axiom is
that {x | x has the same members as some z such that phi(z)} exists
for each stratified phi (the notion of stratification is readily
extended to a language with stratified set abstracts), then any
Forster term model of this theory is extensional (if equality is
defined as "belonging to the same sets"), thus a model of full
stratified comprehension, thus a model of NF (this is the same
argument as above, and it is worth noting that this formulation makes
it clear that the allusions to the finite axiomatizability of NF are
irrelevant to what is being shown; the finite set of operations plays
no essential role).  Forster has shown that there are "Forster term
models" of some extremely weak fragments of NF.  My stricture on any
appeal to this notion is that I cannot see that there is any reason to
believe that simple type theory with infinity (with constants for each
type 0 object) has Forster term models, so I see no reason to think
that NF does.

Further, I answer Gordeev's claim that proof theory gives a reason for
NF to be stronger than NFU + Infinity: cut elimination for NF - Ext
(NF with no extensionality at all) is relatively easy.  Cut
elimination for NF indeed has not been shown (this would show
Con(NF)), but neither has cut elimination for NFU + Infinity, with its
weak extensionality axiom, been shown.  This does not provide evidence
that NFU + Infinity is an extremely strong theory, because this is
known to be false; so it cannot provide any evidence that NF is
especially strong, either.  (Vladimir Vayl claims to have proven
cut-elimination for NFU; this is not the case, as one can discover by
reading what he actually did prove).

By the way, this is not to say that I don't think that a proof of
Con(NF) might be obtained by proving cut elimination for NF; I think
such an attack has promise (I couldn't do it when I tried, but I wish
Gordeev luck in his attempts!).  I don't think that this will result
in a proof that NF is absurdly strong, though: I am morally certain
that NF will come in quite low on the Zermelo hierarchy if it is shown
to be consistent in this way.

--Randall Holmes