Busy Beaver上界证明长度
Upper-Bounding Proof Length with the Busy Beaver
摘要：
考虑一个简短的定理，即一个可以用几个符号写下来的定理。它的最短证明可以任意长吗？我们对这个问题的回答是否定的。受Calude et al（1999）和Chaitin（1984）关于构造$Π_1$句子的第一个反例的上界作为句子长度的函数的论点的启发，我们提出了关于任意陈述的证明长度的类似论点。与上面一样，我们的边界是不可计算的，因为它使用了Busy Beaver oracle。与上面不同的是，我们的结果不限于任何复杂性类。最后，我们将上述搜索过程组合成一个自动（尽管不可计算）的过程来发现哥德尔句子。
英文摘要：
Consider a short theorem, i.e. one that can be written down using just a few symbols. Can its shortest proof be arbitrarily long? We answer this question in the negative. Inspired by arguments by Calude et al (1999) and Chaitin (1984) that construct an upper bound on the first counterexample of a $Π_1$ sentence as a function of the sentence's length, we present a similar argument about proof length for arbitrary statements. As with the above, our bound is uncomputable, since it uses a Busy Beaver oracle. Unlike the above, our result is not restricted to any complexity class. Finally, we combine the above search procedures into an automatic (albeit uncomputable) procedure for discovering Gödel sentences.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
