Upper-Bounding Proof Length with the Busy Beaver

TL;DR

This paper establishes an uncomputable upper bound on the shortest proof length of short theorems using a Busy Beaver oracle, extending previous work and enabling automatic discovery of G"odel sentences.

Contribution

It introduces a novel uncomputable proof length bound applicable to all statements, inspired by Busy Beaver arguments, and combines search procedures for G"odel sentence discovery.

Findings

Proof length of short theorems is bounded by an uncomputable function.

The bound is derived using a Busy Beaver oracle, not limited by complexity classes.

An automatic procedure for discovering G"odel sentences is proposed.

Abstract

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 $\Pi_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\"{o}del sentences.