利用忙闲狸猫数界定证明长度的上界
逻辑
2014-06-10 v1 计算机科学中的逻辑
摘要
考虑一个简短的定理，即仅用少数几个符号即可写出的定理。其最短证明的长度是否可以任意长？我们对这一问题给出否定回答。受 Calude 等人 (1999) 和 Chaitin (1984) 论证的启发，他们构建了 语句的第一个反例作为语句长度函数的上界，我们针对任意语句的证明长度提出了类似的论证。与上述工作一样，我们的上界是不可计算的，因为它使用了忙闲狸猫 (Busy Beaver) 预言机。与上述工作不同的是，我们的结果不受任何复杂度类的限制。最后，我们将上述搜索过程结合成一种自动（尽管不可计算）的过程，用于发现 G"{o}del 语句。
关键词
引用
@article{arxiv.1406.1808,
title = {Upper-Bounding Proof Length with the Busy Beaver},
author = {Gustavo Lacerda},
journal= {arXiv preprint arXiv:1406.1808},
year = {2014}
}
备注
2 pages