# How long can proofs be?

Let $$f(n) = \max\{\text{length of shortest proof of }\varphi \mid \varphi \text{ is a provable ZFC sentence of length } \leq n\}$$

How fast does $$f$$ grow? Is it polynomial, exponential, more than exponential, etc.?

• I appear to have been out-sped :P But I'll remark here what I would have put at the end of my answer: the function you're describing is related to the busy beaver function, and because busy beavers are taught in a lot of CS classes, you will probably have more luck googling for it, even if it isn't on-the-nose what you're interested in. – HallaSurvivor May 12 at 15:41

This function grows really fast: there is no computable function which bounds it!

To see this, note that if we had a computable bound on $$f$$ we could tell whether a sentence $$\sigma$$ is consistent with $$\mathsf{ZFC}$$ (just search over all proofs of length $$ for a $$\mathsf{ZFC}$$-proof of $$\neg\sigma$$). But from this information we could in turn build a computable complete consistent extension of $$\mathsf{ZFC}$$:

• Fix an appropriate enumeration $$(\sigma_i)_{i\in\mathbb{N}}$$ of the sentences in the language of set theory.

• Define a new sequence $$(\tau_i)_{i\in\mathbb{N}}$$ of sentences by recursion as follows:

• $$\tau_0=\sigma_0$$ if $$\sigma_0$$ is consistent with $$\mathsf{ZFC}$$, and $$\tau_0=\neg\sigma_0$$ otherwise.

• $$\tau_{i+1}=\sigma_{i+1}$$ if $$\sigma_{i+1}\wedge\bigwedge_{j\le i}\tau_i$$ is consistent with $$\mathsf{ZFC}$$, and $$\tau_{i+1}=\neg\sigma_{i+1}$$ otherwise.

• The set $$\{\tau_i:i\in\mathbb{N}\}$$ is then a complete computable consistent theory containing $$\mathsf{ZFC}$$ (note that when $$\sigma_i$$ is an axiom of $$\mathsf{ZFC}$$ we'll have $$\tau_i=\sigma_i$$).

However, this contradicts the first incompleteness theorem. (Or Church's theorem, if you like - basically the above is the proof of Church's theorem from the first incompleteness theorem.)

Note that we really used very little about $$\mathsf{ZFC}$$ here. The first incompleteness theorem applies to a huge range of theories, ranging from much weaker than $$\mathsf{ZFC}$$ to much stronger than $$\mathsf{ZFC}$$; briefly, any consistent computably axiomatizable theory which satisfies a very mild technical "strength condition" (basically: at least as powerful as Robinson's $$Q$$) is subject to this phenomenon. See section $$4$$ of this paper of Beklemishev for more details on this point.

To be precise, the form of the first incompleteness theorem I'm using is: "Every computably axiomatizable consistent theory which interprets Robinson's $$\mathsf{Q}$$ is incomplete." Note that we don't need an $$\omega$$-consistency assumption here; while present in Godel's original proof, it was later removed by Rosser.

• It may be useful for the OP note explicitly that the first two sentences of this answer (with $f(|\sigma|+1)$ because $\neg\sigma$ is one symbol longer than $\sigma$) answer the question not only for ZFC but for any undecidable but computably axiomatizable theory. Examples range from Robinson's Q up to ZFC plus any large cardinal axiom that's consistent with ZFC. – Andreas Blass May 12 at 16:46
• @AndreasBlass Edited, thanks! – Noah Schweber May 12 at 16:51
• Hmm why don't you just say that you can computably decide whether a sentence over ZFC is a theorem or not? Saves the trouble of building a computable complete extension. =) – user21820 May 13 at 3:57
• Can you please add the last step of the proof, which is (as far as I understand this proof) that this construction is in contradiction to the incompleteness theorem? I feel like this closes the proof but is left more or less implicit here. – kutschkem May 13 at 11:29
• @MacRance I wasn't using Church's theorem since in my experience it's less well-known. The argument I wrote out basically is the proof of Church's theorem. – Noah Schweber May 13 at 16:54