哥德尔第一不完备定理“真但不可证”版本的简单字符串证明
计算机科学中的逻辑
2014-05-23 v2
摘要
本文提出了哥德尔第一不完备定理一个版本的相当简单 yet 严谨的证明。该版本表述为：“任何包含 0、1、+、*、=、逻辑与、逻辑非及全称量词的自然数递归可枚举理论，要么证明了一个假命题，要么无法证明一个真命题”。证明首先展示了关于有限字符串理论的类似结果，然后通过利用自然数对字符串及其连接进行建模，将其迁移到自然数理论中。证明系统通过图灵机来表达，当且仅当输入字符串为定理时图灵机停机。这种方法使得除一个部分外的所有证明步骤都能通过简单直接的构造简要呈现。细节需要一些谨慎处理，但不需要深厚的背景知识。缺失的部分是图灵机能够执行复杂计算任务这一广为人知的事实。
引用
@article{arxiv.1402.7253,
title = {A Simple Character String Proof of the "True but Unprovable" Version of G\"odel's First Incompleteness Theorem},
author = {Antti Valmari},
journal= {arXiv preprint arXiv:1402.7253},
year = {2014}
}
备注
In Proceedings AFL 2014, arXiv:1405.5272