A Machine-Assisted Proof of G\"odel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets

TL;DR

This paper presents a formal, machine-assisted proof of G"odel's incompleteness theorems within hereditarily finite set theory using Isabelle, marking the first mechanical verification of the second theorem and aiding logicians with detailed formal proofs.

Contribution

It provides the first formal, mechanical proof of G"odel's second incompleteness theorem using Isabelle and hereditarily finite set theory, addressing technical challenges and enhancing proof rigor.

Findings

First mechanical verification of G"odel's second incompleteness theorem

Formalisation follows Swierczkowski's detailed proof in hereditarily finite sets

Addresses technical issues specific to hereditarily finite set theory

Abstract

A formalisation of G\"odel's incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows {\'S}wierczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of this theory is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.