Razonamiento formalizado

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.