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:
A seminar on the proof-method is here:
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 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: Dec 07 2023 at 08:19 UTC