Re: [isabelle] More on "References about mistakes and gaps in papers"
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.
On Tue, May 26, 2020 at 10:42 AM Manuel Eberl <eberlm at in.tum.de> wrote:
> 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. :)
> On 26/05/2020 11:24, Andrei Popescu wrote:
> > 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and