期刊
JOURNAL OF AUTOMATED REASONING
卷 55, 期 1, 页码 1-37出版社
SPRINGER
DOI: 10.1007/s10817-015-9322-8
关键词
Godel's incompleteness theorems; Isabelle/HOL; Nominal syntax; Formalisation of mathematics
An Isabelle/HOL formalisation of Godel's two incompleteness theorems is presented. The work follows Aewierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory (Dissertationes Mathematicae 422, 1-58, 2003). 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 (Logical Methods in Computer Science 8(2:14), 1-35, 2012) is shown to scale to a development of this complexity, while de Bruijn indices (Indagationes Mathematicae 34, 381-392, 1972) 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.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据