The consistency of NF: meeting in Cambridge

Back in October, I posted a slightly mysterious message noting that Thomas Forster was “in the process of assembling funding for a meeting to discuss and broadcast recent developments in NF” here in Cambridge this Easter. Then in November I was able to reveal more, for Randall Holmes had by then announced “I believe that I am in possession of a fairly accurate outline of a proof of the consistency of New Foundations” and it was this which was to be the topic of the Easter gathering. So: how did the meeting go? For various reasons, I wasn’t there, but here’s a report from Thomas Forster:

It went very well.  It didn’t achieve everything I dreamed of, in that I didn’t come away from the meeting understanding the proof — not entirely.  I understand the strategy and I can see why the strategy should work, but I am a long way from understanding the details.

It involves a Ramsey argument like that used by Randall in his ‘tangled types’ paper (which reduces the consistency problem for NF to the task of finding a model of ZFU with some very delicate combinatorial properties).  It then uses an iterated Fraenkel-Mostowski construction to obtain the desired model of ZFU.

My Ph.D. students and I have a weekly meeting in which we press on with “our exagmination round his factification”.  Meanwhile people ask “Do you believe the proof?” and my reply is  “Not yet, but I believe that I will believe it”.  It is a very large proof.  When written out properly it will be 50-60 pages – possibly more — and certainly not 10-15.

Randall is rejigging the presentation in the light of the audience reaction in Cambridge; there is a cunning plan to get one of the theorem-proving communities to embark on a mechanisation  … and the lads and I have a project to write out a version for our own satisfaction.

I expect that by the end of this year I will understand it, and Randall will have sent off a paper to the JSL.

This entry was posted in This and that. Bookmark the permalink.

One Response to The consistency of NF: meeting in Cambridge

  1. That makes me feel a bit better about missing the meeting myself: I would not have come away with an acceptably clear understanding of the proof anyways (if Thomas didn’t, then certainly neither would I). I expect that eventually this proof will be simplified and boiled down to terms understandable by mere mortals.

Leave a Reply

Your email address will not be published. Required fields are marked *