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)设定理论的理论的理论之后完成的。 避免通常的语法计算编码, 消除了在嵌入逻辑计算中将基本数字理论正规化的必要性。 伊莎贝尔正规化使用两种不同的变量约束处理法: 标称软件包显示为这一复杂性的发展规模, 而德布鲁伊恩的指数则显示为用于编码语法的理想。 伊莎贝尔证据的关键细节, 特别是文献中发现的差距和错误 。

0
下载
关闭预览

相关内容

专知会员服务
52+阅读 · 2020年9月7日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
资源|斯坦福课程:深度学习理论!
全球人工智能
17+阅读 · 2017年11月9日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
已删除
将门创投
8+阅读 · 2017年7月21日
Arxiv
0+阅读 · 2021年6月16日
VIP会员
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
Ray RLlib: Scalable 降龙十八掌
CreateAMind
9+阅读 · 2018年12月28日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Hierarchical Disentangled Representations
CreateAMind
4+阅读 · 2018年4月15日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
资源|斯坦福课程:深度学习理论!
全球人工智能
17+阅读 · 2017年11月9日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
已删除
将门创投
8+阅读 · 2017年7月21日
Top
微信扫码咨询专知VIP会员