Email Gateway (Aug 23 2022 at 09:01): Email Gateway (Aug 23 2022 at 09:01):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Hi Manuel,
I was thinking of that too. In fact, I was even thinking of eventually
working with Johannes and Arve to import their HOL4 proof and combine
it with my own "patch", which is formalized in Isabelle.
Cheers,
Andrei
Email Gateway (Aug 23 2022 at 09:12):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Dear all,
This message's subject refers to an old thread on the Isabelle mailing
list, from July 2018. This time, I and my coauthor are the
protagonists of some "mistakes and gaps"...
In impressive recent work,
https://arxiv.org/abs/2002.10212
Johannes Åman Pohjola and Arve Gengelbach have formalized in HOL4 our
model-theoretic proof of consistency for (an abstract representation
of) Isabelle/HOL's logic (http://andreipopescu.uk/pdf/ITP2015.pdf).
They have found three errors in our informal proof. Two involved
subtleties about variable names and substitution and were fairly easy
to fix. The third one was more serious, and they have fixed it by
adding a new clause to the definitional dependency relation. Please
see their paper for details.
Best wishes,
Andrei
PS. Incidentally, in the meantime I had also discovered the more
serious problem (which affects three of our papers), and I had
formalized in Isabelle a different fix -- the fix only, not the whole
proof (http://andreipopescu.uk/Theories/Fix_Comp_IHOL_Cons.zip). I
will soon produce an errata, reflecting Johannes and Arve's findings
as well.
Email Gateway (Aug 23 2022 at 09:13):From: Manuel Eberl <eberlm@in.tum.de>
In that light, it seems serendipitous indeed that Jonas, Fabian, and
Makarius are working on (and have been making good progress with)
importing HOL4 developments into Isabelle/HOL.
That means we could actually have a consistency proof of Isabelle/HOL
within itself (modulo the usual Gödelian caveats, of course).
Nice. :)
Manuel
Last updated: Apr 27 2024 at 01:05 UTC