jamie gabbay (Apr 07 2022 at 09:11): jamie gabbay (Apr 07 2022 at 09:11):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.
Kevin Kappelmann (Apr 07 2022 at 10:51):Hi Jamie,
jamie gabbay (Apr 07 2022 at 13:30):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: Apr 20 2024 at 08:16 UTC