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.?

Solution 1:

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 $<f(\vert\sigma\vert+1)$ 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.