FOM: Is reasoning in NF "tricky"?

[holmes@catseye.idbsu.edu]

Kanovei asserted fairly recently that 

>NF is perhaps the only known alternative to ZFC as foundations, 
>but it so drastically contradicts practice of mathematical 
>reasoning that almost everything simple in ZFC (and "naive" mathematics) 
>needs tricky reasoning in NF. 

Any reasoning which can be carried out in the theory of types can be
reproduced faithfully in NF.  This covers a lot of simple reasoning in
mathematics.

There is a fairly simple proof of Infinity in NF (not requiring the
full "trickiness" of Specker's disproof of Choice).  Given this proof,
one has the ability to reproduce in NF every proof in the
impredicative theory of types with Infinity.

This is sufficient to cast serious doubt on Kanovei's assertion above.
The theory of types with Infinity is enough to do everything in 
"naive" mathematics in a fairly straightforward manner, though in a
style to which the ZFC practitioner is not accustomed, and hampered
by the absence of choice.

A better approach is to work with NF + Rosser's Axiom of Counting (the
assertion that any finite set is the same size as its image under the
singleton operation).  Rosser's axiom is "intuitive" and has infinity
as a fairly immediate corollary, eliminating the only "tricky" element
in the indicated approach.

NFU + Rosser's axiom is even better, since it is known to be
consistent (rel weak fragments of ZFC) and not especially strong.
Rosser's axiom eliminates most technical problems with stratification
relevant to "naive mathematics".  Moreover, this theory is also
consistent with choice (NF is not).

I'm not saying that reasoning in NF (or NFU) isn't tricky for the
ZFC practitioner.  Attention to stratification is not something the
ZFC practitioner is used to, and mistakes can be made.  But this is
a matter of changing habits, not a matter of intrinsic difficulty.

There are various results in NFU or ZFC which are false when
literally translated into the other system.  In most such cases, the
point is that the literal translation of a result is not the
appropriate translation.  The correct translation of a result from ZFC
into NF or NFU can usually be determined by thinking about how the
result would be expressed in type theory.  (In comparisons of ZFC and
NFU, one also needs to take into account the difference in consistency
strength; a better comparison in this respect would be between NFU +
Infinity + Choice and Zermelo set theory with bounded comprehension; NF
is not known to be any stronger than this, but of course the failure
of choice in NF makes analogies more difficult).

It is also a very doubtful assertion that NF is the only known
alternative foundation.

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