Incompleteness Theorems (Q40326)

Gödel's two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets . This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument. Löb's theorem states that we have that $\mathsf{HF} \vdash \mathsf{PfP}(\ulcorner \varphi \urcorner) \rightarrow \varphi$ implies $\mathsf{HF} \vdash \varphi$, where the formula $\mathsf{PfP}(x)$ is the standard provability predicate for $\mathsf{HF}$. It is a strengthening of Gödel's second incompleteness theorem, which can be recovered via $\varphi := \bot$. The formalised argument follows a modern textbook presentation of Löb's argumentation by Smith via the Hilbert-Bernays-Löb derivability conditions. The formalisation of Löb's theorem is part of Janis Bailitis's Bachelor's thesis completed at Saarland University in 2024.