diff --git a/Nfproof/maybedetangled2.pdf b/Nfproof/maybedetangled2.pdf index 74d8fac..1715d95 100644 Binary files a/Nfproof/maybedetangled2.pdf and b/Nfproof/maybedetangled2.pdf differ diff --git a/Nfproof/maybedetangled2.tex b/Nfproof/maybedetangled2.tex index 4942640..c86007f 100644 --- a/Nfproof/maybedetangled2.tex +++ b/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/5/2024:] Updates to the postscript. + \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)$. @@ -1384,14 +1386,14 @@ \section{Conclusions, extended results, and questions} \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. +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, but 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. +NFU is serviceable as a foundation for mathematics, and consistent with Choice and various strong axioms of infinity. It is odd that NFU + Choice proves that there are urelements (the same odd fact that NF disproves Choice), but no more than odd. +The type discipline of stratification is something that one must work to get used to, 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).