2014/06/06 by Gustavo Lacerda, Lacerda, Gustavo
Computer Science · #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Natural Language Processing Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1406.1808
openalex publication_date 2014/06/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.