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. _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
