NF draft

Nfproof/maybedetangled2.tex

@@ -47,6 +47,8 @@ \subsection{Dated remarks on versions}
 {\bf initial note for the previous series:}  This document is probably my best overall version so far.  The immediate occasion for its preparation was to serve students attempting to verify the proof in Lean.  A formal verification should avoid metamathematics, so it is the fact that the structure defined in section 3 is a model of TTT which should be verified, and further, a finite axiomatization (mod type indexing) of TST and thus TTT should be verified in the model in lieu of the usual statement of the axiom of comprehension of TTT.  {\bf This program has been completed, on the Lean side.}
 \begin{description}
 
+\item[5/3/2024:]  Added a postscript commenting on philosophical relevance.
+
 \item[4/30/2024:]  Sky points out that formalizing the new cardinal parameter conditions requires $\lambda \leq {\tt cf}(\mu)$.
 Text is revised to address this need.
 
@@ -1380,6 +1382,27 @@ \section{Conclusions, extended results, and questions}
 
 Another question of a very general and amorphous nature which remains is:  what do models of NF (or TTT) look like in general?  Are all models of NF in some way like the ones we describe, or are there models of quite a different character?  There are very special assumptions which we made by fiat in building our model of TTT which do  not seem at all inevitable in general models of this theory.
 
+\subsection{Postscript}
+
+Inevitably, philosophical issues come up in connection with a system of set theory proposed by a philosopher.  I get a lot of congratulations for vindicating Quine's foundational agenda, and in fact this is not part of my purpose here.  It is not even clear to me that Quine {\em had\/} a foundational agenda in which his technical proposal of this set theory had a special place.
+
+The results of this paper show that if one really wanted to, one could use NF as a foundation for mathematics.  It is odd that it disproves Choice, but the principle ``power sets of well-orderable sets are well-orderable", which holds in models constructed in this way, supports most applications of Choice.
+
+Our opinion is that Quine's proposal of NF was based on a mistake.  He discusses whether to assume strong extensionality in the original paper, and his explanation of reasons for choosing strong extensionality contains an actual mathematical error.  We believe that the correct system to propose was NFU, and if he had proposed NFU, the history of this kind of set theory might have been different.
+
+NFU is serviceable as a foundation for mathematics, and consistent with Choice and various strong axioms of infinity.
+The type discipline of stratification is unfamiliar, and it has been remarked that working with indexed families of sets is extremely awkward in NFU (and would be similarly awkward in NF).  The view of the world which NFU supports is basically the same as that of ZFC:  the natural models of NFU are obtained by considering an initial segment of the cumulative hierarchy with an external automorphism which moves a level, and NFU can interpret discussion of exactly such a structure internally.
+
+Unlike NF, NFU on introspection can tell one quite a lot about what its models should look like (as ZFC can with its own awareness of initial segments of the cumulative hierarchy; in NFU, analysis of the isomorphism classes of well-founded extensional relations gives both an interpretation of an initial segment of the Zermelo style universe and an interpretation of NFU itself if one has strong enough assumptions).    NF tells one very little about what its intended world is like (it can, being an extension of NFU, internally construct a lot of information about an interpretation of NFU with lots of urelements, but there is not an obvious way to find out how an extensional world is constructed from internal evidence in NF itself).
+
+So, we do not believe this paper is a philosophical milestone.  If there was one, it happened in 1969 when Jensen showed that NFU is consistent, and nobody noticed.
+
+We do believe that there are interesting questions to investigate about NF.  Our paper does not settle all the questions about this system which have developed in the minds of people who have worked with it since 1937.  In fact, the construction is based on special assumptions  and does not seem to give much of an idea of what general models of this theory might look like.
+
+It might be viewed as philosophically interesting that this proof was formally verified.  That is really an advertisement for a quite different foundational system, the logic of the Lean proof verification system.   That it needed to be formally verified I believe reflects an interesting complexity in the mathematics here, not only the deficiencies of the first author as an expositor.
+
+
+
 \newpage
 
 \begin{thebibliography}{99}