Reseña: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle
Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre metalógica titulado A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.
Su autor es Lawrence C. Paulson (de la Univ. de Cambridge, Inglaterra).
Su resumen es
An Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. The work follows Swierczkowski’s detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package is shown to scale to a development of this complexity, while de Bruijn indices turn out to be ideal for coding syntax. Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature.
El código de las correspondientes teorías en Isabelle se encuentra aquí.