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.

翻译：G\“odel”的两个不完全性理论的伊莎贝尔/HOL正式化。 工作是在\\ swierczkowski 详细证明使用本性有限(HF)设定理论的理论的理论之后完成的。 避免通常的语法计算编码, 消除了在嵌入逻辑计算中将基本数字理论正规化的必要性。 伊莎贝尔正规化使用两种不同的变量约束处理法: 标称软件包显示为这一复杂性的发展规模, 而德布鲁伊恩的指数则显示为用于编码语法的理想。 伊莎贝尔证据的关键细节, 特别是文献中发现的差距和错误 。