First-order logic completeness for the lazy programmer

PorJosé A. Alonso

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.

A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

A Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. Aspects of the development are described in detail, including two separate treatments of variable binding: the nominal package and de Bruijn indices. The work follows Świerczkowski’s a detailed proof, using hereditarily finite set theory.

The machine proofs are fairly readable, thanks to the structured Isar proof language, and concise at under 14,000 lines for both theorems. The paper presents highlights of the proof, commenting on the advantages and disadvantages of the nominal framework and HF set theory. The proof reported here closely follows a detailed exposition by Świerczkowski. His careful and detailed proofs were indispensable, but significant deviations proved to be necessary. For the first time, we have complete, formal proofs of both theorems. They take the form of structured Isar proof scripts that can be examined interactively.

The total proof length of 14000 lines comprises 5000 lines for the second theorem and 9000 lines for the first. (One could also include 3000 lines for HF set theory itself, but then we may as well also count the standard libraries of natural numbers.)

This project took approximately one year, in time left available after fulfilling a Professor’s usual teaching and administrative duties. The underlying set theory took only two weeks to formalise. The Gödel development up to the proof formalisation condition took another five months. From there to the first incompleteness theorem took a further two months, mostly devoted to proving single valued properties. Then the second incompleteness theorem took a further four months, including much time wasted due to misunderstanding this perplexing material.