One of the responses to my Mathoverflow question No. 122658 hinted that a proof (or the outline of a proof) of the consistency of NF relative to ZF was on the horizon and was to be presented at a meeting in Cambridge scheduled for April of this year. Does anyone have additional information about this?
$\begingroup$
$\endgroup$
6
asked May 28, 2013 at 14:23
-
$\begingroup$ Have you tried contacting Randall Holmes? $\endgroup$– Ryan BudneyCommented May 28, 2013 at 14:26
-
2$\begingroup$ Here's a relevant post from the same blog that Joel David Hamkins cited as his source in his answer to your previous question: logicmatters.net/2013/04/… $\endgroup$– j.c.Commented May 28, 2013 at 14:39
-
2$\begingroup$ plus.google.com/103404025783539237119/posts/c6QbY9MpNJK Randall has a manuscript, that is still only being privately circulated while it is polished. If you email him directly, most likely he will email you a copy. $\endgroup$– Andrés E. CaicedoCommented May 28, 2013 at 15:02
-
$\begingroup$ Thanks alot for the updates. I hope for the best possible outcome. If it should occur, perhaps people will start looking deeply into NF, just as they have done with ZF. $\endgroup$– Garabed GulbenkianCommented May 29, 2013 at 15:30
-
$\begingroup$ Here's the link to Randall's FOM announcement, in case you're interested: cs.nyu.edu/pipermail/fom/2012-November/016758.html. $\endgroup$– Zach NCommented May 31, 2013 at 6:40
|
Show 1 more comment
3 Answers
$\begingroup$
$\endgroup$
4
It has indeed been exhausting. I can report that the situation seems to have been resolved. The central hard part of the latest version of my Con(NF) proof has been verified in Lean by Sky Wilshaw, a Part III student at Cambridge. There remains the substantial project of cleaning up the paper (which has been improved by two years of dialogue with the verifier) and tidying up the formalization and making all available. But I can report firmly that the result is correct.
-
8$\begingroup$ Detail: I believe that NF is no stronger than bounded Zermelo set theory with infinity (the strength claim quoted above) but my proof does not show that. It requires enough replacement for the existence of beth_omega_1. $\endgroup$ Commented May 1 at 14:21
-
$\begingroup$ Just out of curiosity: it really needs $\beth_{\omega_1}$, and not $\beth_\alpha$ for all countable $\alpha$? I ask because Borel Determinacy is often said to need Replacement for functions on $\omega_1$, but it turns out to only need Replacement for all countable ordinals. The answer is almost surely that you do need this beth, but I'm just wanting confirmation for this tiny itch. $\endgroup$– David Roberts ♦Commented May 2 at 12:17
-
$\begingroup$ As far as I can tell, I need beth_omega_1. It might be possible to finesse things in the way you describe, but the problem is so hard that I just want a solution that works $\endgroup$ Commented May 3 at 18:42
-
$\begingroup$ Fair enough! I've been following your travails since the announcement, and I cannot but admire your tenacity, and cannot complain if the proof is not 100% optimised! $\endgroup$– David Roberts ♦Commented May 4 at 3:01
$\begingroup$
$\endgroup$
3
So the situation has changed dramatically! I'm not an NF-expert even remotely, so I can't comment on what follows, but:
Randall Holmes has now posted (EDIT: this is unintentionally misleading, see Thomas' answer below) his proof of the consistency of NF: http://math.boisestate.edu/~holmes/holmes/nfisconsistentbytangledtypes.pdf. The proof is quite long, and to the best of my knowledge has not been fully vetted, but it was circulated privately for some time (as mentioned in the comments) so I am optimistic.
While Holmes' proof was circulating, James Gabbay posted a proof of the consistency of NF: http://arxiv.org/abs/1406.4060. His proof is also quite long, but he has slides provide a nice (and funny!) summary of the argument: http://gabbay.org.uk/talks/20141022-leeds-2.pdf. EDIT: But see Andres' comment below.
Holmes' (purported) proof is relative to much less than ZF, I believe to the theory TST which is roughly as strong as Zermelo set theory Z; Gabbay's (purported) proof is relative to ZF, but likely uses nothing beyond Z.
The thread http://www.cs.nyu.edu/pipermail/fom/2014-July/thread.html#18026 at the mailing list FOM discusses both proofs, although not in detail.
answered Jul 28, 2015 at 20:22
-
7$\begingroup$ Gabbay withdrew his paper a while ago. $\endgroup$ Commented Jul 28, 2015 at 23:28
-
$\begingroup$ Oh, I was not aware of this - does he believe his argument may be fixable? $\endgroup$ Commented Jul 28, 2015 at 23:34
-
2$\begingroup$ Gabbay has been privately circulating a possible fix to his proof among NFistes, but it's still not vetted. Also, Holmes suspects NF May actually be equiconsistent to Mac Lane set theory, but this is just his best guess. $\endgroup$ Commented Jul 29, 2015 at 3:57
$\begingroup$
$\endgroup$
6
Saying that Randall Holmes has now posted his proof of the consistency of NF is misleading. He has posted five different proofs at his homepage http://math.boisestate.edu/~holmes/, and explains
The difficulty is not that I do not know how the proof goes...this I am fairly certain about; what is unclear is how to lay it out so that another human being can understand it. Different approaches suggest themselves, and I have tried several.
The oldest of these proofs has been published before July 2014, see http://www.cs.nyu.edu/pipermail/fom/2014-July/018031.html.
All five versions contain a section Conclusions to be drawn about NF including the following paragraph
It seems clear that this argument, suitably refined, shows that the consistency strength of NF is exactly the minimum possible on previous information, that of TST + Infinity, or Mac Lane set theory (Zermelo set theory with comprehension restricted to bounded formulas). Actually showing that the consistency strength is the very lowest possible might be technically tricky, of course. I have not been concerned to do this here. It is clear from what is done here that NF is much weaker than ZFC.
The Conclusions section of Gabbay's paper includes the following paragraph
Given our proof, we can examine it to see how much set-theoretic strength it really uses, and thus see relative to what system we have proved NF consistent. We have not used the Axioms of Choice or Replacement in the proofs of this paper: we have proved NF consistent relative to Zermelo set theory (Z).
Note that consistency relative to Zermelo set theory is not the minimum possible, which would be Mac Lane set theory (Zermelo set theory with comprehension restricted to bounded formulas). It remains unclear whether Gabbay just didn't care about this detail, or whether his proof really uses comprehension for unbounded formulas in an essential way.
Andres Caicedo indicates that Gabbay withdrew his paper a while ago. However, http://www.gabbay.org.uk/papers.html#submitted still links to a version of the proof from May 2015. I guess that Gabbay's proof simply should not appear in a journal before one of Randall Holmes proofs, because those are older and have been checked much more thoroughly by many more mathematicians.
This question raises the general issue what must be done before a long standing open problem can be declared as solved. As long as the author of the proof is not yet satisfied with the presentation of his proof and still makes steady progress towards a better presentation, either waiting patiently for a final version, or reading and trying to understand a preliminary version seem to be reasonable options.
-
2$\begingroup$ One could think of Randall's as a proof by exhaustion: Nobody has found a mistake because everybody got tired of all the changes in the manuscript and stopped looking. $\endgroup$ Commented Jul 29, 2015 at 1:36
-
3$\begingroup$ @AndresCaicedo Do you know whether the "everybody" in your comment includes Bob Solovay? The reasons I ask are that (1) I understand that he paid attention to some of Randall Holmes's earlier work on NF, so he would presumably be interested in the consistency result, and (2) his reputation for careful work leads me to think that, if he were to say that he's studied the proof and thinks it's correct, that would be a huge step toward general acceptance of the proof. $\endgroup$ Commented Jul 29, 2015 at 2:05
-
2$\begingroup$ Hi Andreas. I believe Bob has decided to wait for a published account before trying to study the argument again. $\endgroup$ Commented Jul 29, 2015 at 3:01
-
3$\begingroup$ @Andres: Amusingly, there were a few meetings of the Cambridge DPMMS's set theory seminar that ended up spent mostly on trying to sort out different drafts of Randall's proof. I like to think our consequent harassment resulted in some readability improvements over the winter... $\endgroup$ Commented Jul 29, 2015 at 4:14
-
6$\begingroup$ These comments are bracing for me, but quite fair! $\endgroup$ Commented May 1 at 14:24