Gödel不完备性定理的一种机械化证明
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
摘要：
一个伊莎贝尔/HOL形式化哥德尔的两个不完全定理。这项工作遵循Zeriwierczkowski的详细证明定理使用遗传有限（HF）集理论。避免通常的算术编码的语法消除了形式化的必要性，在嵌入式逻辑演算的初等数论。伊莎贝尔形式化使用两个单独的治疗变量绑定：标称包的规模，以发展这种复杂性，而德Bruijn指数原来是理想的编码语法。伊莎贝尔证明的关键细节进行了描述，特别是在文献中发现的差距和错误。
英文摘要：
An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is presented. The work follows Świerczkowski'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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
