Stream: General

Topic: Seeking Isabelle ConNF formalisation


view this post on Zulip 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.

view this post on Zulip Kevin Kappelmann (Apr 07 2022 at 10:51):

Hi Jamie,

  1. 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.
  2. 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)
  3. 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.

view this post on Zulip jamie gabbay (Apr 07 2022 at 13:30):

Hi Kevin. Thanks for your message.

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

Yes, thank you.

  1. 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.

  1. 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: Sep 25 2022 at 23:25 UTC