Coq验证的算术基本不完备
摘要：哥德尔-罗瑟不完备性定理的一种构造性证明已经使用Coq证明助手完成。对任意语言的经典一阶逻辑的某些理论进行了形式化。给出了原始递归函数的发展，并证明了所有原始递归函数可以在弱公理系统中表示。将公式和证明编码为自然数，并证明操作这些编码的函数是原始递归的。证明了这个弱公理系统基本上是不完全的。特别地，在Coq的类型理论中证明了皮亚诺算术是一致的，因此是不完全的。
作者：Russell O'Connor
论文ID：cs/0505034
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2008-05-19