First-order logic completeness for the lazy programmer

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado First-order logic completeness for the lazy programmer.

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

Su resumen es

Codatatypes are regrettably absent from 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.