The consistency of NF (Gabbay claimed proof)

Stream: maths

[jamie gabbay]

Hello all. This is Jamie Gabbay. I have a claimed proof of the consistency of Quine's NF.

Details of the proof-method are here:
https://arxiv.org/pdf/1406.4060
A seminar on the proof-method is here:
https://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars/lfcs-seminars-2022/lfcs-seminar-29-march-2022-jamie-gabbay
https://www.youtube.com/watch?v=CzAw3gBry08

Quine's NF is a set-theory/type-theory whose consistency has been an outstanding open problem since 1937. Its distinguishing feature is that it admits a universal set Omega --- thus Omega is an element of Omega.

The structure of the argument in https://arxiv.org/pdf/1406.4060 is as follows: a simple soundness argument, some cut-elimination, saturating a consistent set to a maximal consistent set, and then building an NF model from that maximally consistent set.

I welcome your input on the feasibility of formalising this.

I hope the above is completely clear and I welcome questions, comments, and DMs.

[Yaël Dillies]

Hey! Welcome. @Thomas Forster and @Randall Holmes are organizing an internship for a group of 6-7 Cambridge undergrads (including me) to formalize Randall's proof. See The consistency of NF and con-nf

[jamie gabbay]

Thanks for the heads-up @Yaël Dillies . Please feel free to DM me your impression of the feasibility of formalising my claimed proof.