[isabelle] More on "References about mistakes and gaps in papers"
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,
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.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and