A Mechanised Proof of G\"odel's Incompleteness Theorems using Nominal Isabelle

TL;DR

This paper presents a formal Isabelle/HOL proof of G"odel's incompleteness theorems, avoiding traditional arithmetic encodings by using hereditarily finite set theory and variable binding techniques.

Contribution

It introduces a novel formalisation approach that bypasses elementary number theory, demonstrating the scalability of nominal techniques and identifying gaps in existing literature.

Findings

Successful formalisation of G"odel's theorems in Isabelle/HOL

Comparison of nominal and de Bruijn approaches for syntax encoding

Identification of errors in previous proofs

Abstract

An Isabelle/HOL formalisation of G\"odel'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.