Hello all. This is Jamie Gabbay. Some of you may know me as one of the authors behind the "nominal" in "Nominal Isabelle".

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.

I'd like to offer an opportunity for you work with me on formalising theis proof. You'd learn some unique stuff about foundations, plus a number of useful proof techniques, and (optionally) about Nominal Isabelle. And you'd play a role and be seen to have played a role in establishing original proof of a historically important result.

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

Hi Jamie,

- I suppose you know that some people considered formalising Holme's proof in Lean a month ago? I do not know if someone is now actually working on it.
- Do you think your proof is more amenable to formalisation than Holme's? (I haven't read either one but the latter has been in the pipeline for so long, I suppose it must be intricate)
- Are you planning to use Isabelle/Nominal(2)? I wonder if the benefits of doing so outweighs the disadvantages in comparison to using Isabelle/HOL.

Hi Kevin. Thanks for your message.

- I suppose you know that some people considered formalising Holme's proof in Lean

Yes, thank you.

- Do you think your proof is more amenable to formalisation than Holme's?

Good question. Yes, I expect my claimed proof to be much more amenable to formalisation.

Structurally, the argument requires a simple soundness argument, some cut-elimination, saturating a consistent set to a maximal consistent set, and then building another model from that maximally consistent set.

- Are you planning to use Isabelle/Nominal(2)?

I'd be very pleased to use Nominal Isabelle if this would be convenient, of course, but how we represent NF syntax and derivation is orthogonal to the proof-method so this would be a pragmatic call.

Last updated: Nov 11 2024 at 04:22 UTC