Suppose we want to show that there is a number \(n\) such that no upper bound on the busy beaver number \(\Sigma(n)\) is provable from, say, the axioms of ZFC. One possible proof is as follows: Assume that no such \(n\) exists. That is, assume that for every \(n\), there is a proof in first-order logic that uses only the axioms of ZFC and derives a sentence \(\Sigma(n) \leq m\) for some \(m\). Then we could compute an upper bound for \(\Sigma(n)\) by **exhaustively searching all of the possible valid ZFC proofs** until we found one that deduced a theorem of the form \(\Sigma(n) \leq m\); by assumption, we must eventually find such a proof. But we know that we cannot compute an upper bound on \(\Sigma(n)\) for arbitrary \(n\); thus, we have derived a contradiction, and the original assumption must be false.

Enumerating proofs until you find one with the desired properties is one of those grand CS traditions that, like calling an \(O(n^{12})\) algorithm “efficient” while dismissing an \(O(1.001^n)\) algorithm as “intractable”, is handy for theoretical purposes but has essentially no bearing on the real world whatsoever. After all, **no one would really write a program that loops through all possible proofs and tests each one**.

Right?

Continue reading The shortest proof for every theorem