FOM: extensionality -- re Hazen remarks

[M. Randall Holmes]

Dear FOMers,

Allen Hazen said:

I'm not sure the status of the axiom of infinity is an ISSUE in the
foundations of mathematics.  Maybe in metaphysics/philosophical
logic/philosophy of language, but not for the foundations of mathematics.
Quine's pragmatic approach to this (to give it a name!) issue will probably
be attractive to most FoM workers: in formulating a foundational system for
(classical) mathematics or a fragment of it, you will want to postulate the
existence of something set-ish.  You can call them PROPERTIES (and not
postulate extensionality) if you want, but it's simpler and neater and so
on to postulate extensionality and call them SETS.
This is o.k., because (probably!) adding the extensionality postulate isn't
really begging any questions, and won't smuggle undeclared mathematical
power into your system.  This is because-- not in all imaginable contexts,
but under fairly general assumptions-- a system with extensionality added
can be interpreted in the corresponding system without it, and so doesn't
add serious deductive power or serious risk of inconsistency. [...]

I comment:

Hazen should have remarked that there is one well-known counterexample
to his claims about extensionality.  Jensen's variant NFU of Quine's
"New Foundations" is weaker than Peano arithmetic.  Adding strong
extensionality to NFU yields Quine's NF, which is at least as strong
as the theory of types with infinity (i.e., adds serious deductive
power), or, equivalently, Zermelo set theory with comprehension
restricted to bounded formulas.  Moreover, this adds risk of
inconsistency, because so far we do not know (IMHO have no particular
reason to believe) that NF is consistent.

It turns out, though, that if one takes the theory whose only axiom scheme
is the axiom of stratified comprehension (NF without _any_ extensionality)
that this does interpret NFU (one can get extensionality for nonempty sets
"for free" in Quine-style set theory).  This is a nice observation of Marcel
Crabb\'e -- the argument is very easy but somehow escaped notice until
1990.  So even in the NF world there is something one can say along
the lines of Hazen's remarks above.

(footnote: Quine's observations on strong vs. weak extensionality in
the original "New foundations" paper may be misleading -- they have
the same character as Hazen's remarks above but are mathematically
incorrect.  He claims that it is harmless to identify "urelements"
with their own singletons.  This is wrong on two counts in the context
of NF: the requisite redefinition of membership cannot be carried out
in a stratified manner, and in any event the assumption that each
urelement is a singleton amounts to the assumption that there are not
very many urelements, so is far from trivial (all known models of NFU
have more urelements than singletons, and it is known that the
existence of a model of NFU with no more urelements than sets implies
that NF is consistent).)

                                    --Randall Holmes