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.
Footnote: Boise State where Randall is has no PhD programme in maths. Students excited by this kind of thing can always come to Cambridge do a Ph.D. on NFiste matters with Thomas!
