The status of 'the consistency of NF relative to ZF' 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?
 A: 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.
A: 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.
