33
$\begingroup$

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

$\endgroup$
  • 6
    $\begingroup$ 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. $\endgroup$ – HallaSurvivor May 12 at 15:41
39
+50
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • 3
    $\begingroup$ 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. $\endgroup$ – Andreas Blass May 12 at 16:46
  • $\begingroup$ @AndreasBlass Edited, thanks! $\endgroup$ – Noah Schweber May 12 at 16:51
  • 2
    $\begingroup$ 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. =) $\endgroup$ – user21820 May 13 at 3:57
  • 1
    $\begingroup$ 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. $\endgroup$ – kutschkem May 13 at 11:29
  • 1
    $\begingroup$ @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. $\endgroup$ – Noah Schweber May 13 at 16:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.