Reseña: Coinductive pearl: Modular first-order logic completeness

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

El código de las teorías Isabelle correspodientes se encuentra aquí.