# Interpretation of the Second Incompleteness Theorem

For simplicity, let me pick a particular instance of Gödel's Second Incompleteness Theorem:

ZFC (Zermelo-Fraenkel Set Theory plus the Axiom of Choice, the usual foundation of mathematics) does not prove Con(ZFC), where Con(ZFC) is a formula that expresses that ZFC is consistent.

(Here ZFC can be replaced by any other sufficiently good, sufficiently strong set of axioms, but this is not the issue here.)

This theorem has been interpreted by many as saying "we can never know whether mathematics is consistent" and has encouraged many people to try and prove that ZFC (or even PA) is in fact inconsistent. I think a mainstream opinion in mathematics (at least among mathematician who think about foundations) is that we believe that there is no problem with ZFC, we just can't prove the consistency of it.

A comment that comes up every now and then (also on mathoverflow), which I tend to agree with, is this:

(*) "What do we gain if we could prove the consistency of (say ZFC) inside ZFC? If ZFC were inconsistent, it would prove its consistency just as well."

In other words, there is no point in proving the consistency of mathematics by a mathematical proof, since if mathematics were flawed, it would prove anything, for instance its own non-flawedness. Hence such a proof would not actually improve our trust in mathematics (or ZFC, following the particular instance).

Now here is my question: Does the observation (*) imply that the only advantage of the Second Incompleteness Theorem over the first one is that we now have a specific sentence (in this case Con(ZFC)) that is undecidable, which can be used to prove theorems like "the existence of an inaccessible cardinal is not provable in ZFC"? In other words, does this reduce the Second Incompleteness Theorem to a mere technicality without any philosophical implication that goes beyond the First Incompleteness Theorem (which states that there is some sentence $$\phi$$ such that neither $$\phi$$ nor $$\neg\phi$$ follow from ZFC)?

• In the case of inaccessible cardinals, you can bypass the second incompleteness theorem in the following sense. If an inaccessible exists, then there is a least inaccessible $\kappa$, and its existence is not provable because $V_\kappa$ is a model of ZF+"there is no inaccessible". (I like to call this Zermelo's incompleteness theorem, because he proposed the argument in 1928, before Goedel.) Sep 9, 2010 at 16:45
• @John: But in $V_\kappa$ there are still plenty of (countable, transitive) models of ${\sf ZFC}+$there is an inaccessible'', so this sense of incompleteness is certainly weaker. Sep 9, 2010 at 16:49
• @Stefan: Do you think the first theorem already invalidates Hilbert's program? Sep 9, 2010 at 16:49
• About (*): If we could prove the consistency of ZFC inside ZFC we would have shown the inconsistency of ZFC - and thus gained interesting information, isn't it? Sep 9, 2010 at 17:17
• @Andres: I was thinking that observation (*) already invalidates Hilberts program to some extent (the consistency part). The First Incompleteness Theorem takes care of another issue: No reasonable system of axioms for mathematics is complete. But Andreas below has a real point. Sep 9, 2010 at 19:59

For the philosophical point encapsulated in (*) in the question, it seems that corollaries of the second incompleteness theorem are more relevant than the theorem itself. If we had doubts about the consistency of ZFC, then a proof of Con(ZFC) carried out in ZFC would indeed be of little use. But a proof of Con(ZFC) carried out in a more reliable system, like Peano arithmetic or primitive recursive arithmetic, would (before Gödel) have been useful, and I think this is what Hilbert was hoping for. Gödel's second incompleteness theorem tells us that this sort of thing can't happen (unless even the more reliable system is inconsistent).

• Gentzen's proof of the consistency of PA illustrates another possibility. Conceivably, we might have more confidence in PRA + induction up to $\epsilon_0$ than in PA. We can view the significance of Goedel's 2nd theorem not as entirely ruling out the possibility of a meaningful consistency proof of a theory T, but merely ruling out such a proof in a system that is weaker than T. Of course, the trouble with ZFC is that we have no candidate for a system (1) that is neither stronger than nor weaker than ZFC; (2) that we have more faith in than we have in ZFC; and (3) that can prove Con(ZFC). Sep 27, 2021 at 1:02

The answer is the following observation due to Hilbert:

If we can prove the consistency of $ZFC$ using elementary methods, then any elementary theorem of $ZFC$ has an elementary proof, i.e. we don't need ideal/abstract objects like sets or real number for dealing with concrete/finite objects like numbers.

The importance of Godel's theorems is not that $ZFC$ can't prove its own consistency but rather the weaker result that elementary methods (assuming that listing these methods is easy, i.e. recursively enumerable) cannot prove all elementary results, in other words, we need abstract objects even for doing elementary number theory. Hilbert wanted to show that although abstract objects are helpful for elementary mathematics in practice, they are not essential and can be avoided (at least in theory) if needed. But Godel's first incompleteness theorem already shows that this is not true. (Here elementary can arguably be identified with unbounded-quantifier-free formulas or $\Pi_1$ sentences.)

Yudkowsky and Herreshoff have a (messy but) great paper which relates the second incompleteness theorem to issues in theoretical artificial intelligence. (This paper of mine might be a more accessible introduction to the subject.) In principle, one way an intelligent agent $$M$$ might achieve a goal is by building an auxiliary agent $$M'$$ and tasking it with the goal. But presumably $$M$$ cannot satisfy its criterion for action unless it can prove that $$M'$$ reasons consistently --- otherwise it could be building an agent who might fail because it reasons incorrectly. But by the second incompleteness theorem, $$M$$ cannot prove that the system within which it itself reasons is sound, which means that $$M'$$ would have to reason within a weaker system.

It's especially a problem for the idea of self-modifying AI. A sufficiently advanced AI ought to be better at designing AI's than we are. So we might want to design an AI which is capable of improving itself by modifying its own source code. But the incompleteness obstacle seems to imply that it could only do this at the cost of weakening the formal system in which it reasons. Since proof-theoretic strength is gauged by ordinals, after finitely many iterations it would reach imbecility.

At first sight it seems like there should be a trivial resolution, but the more you think about it, the more serious you realize the problem is.

The fact that the second incompleteness theorem refers to consistency is important for several applications, both philosophical and mathematical.

Philosophically, the second incompleteness theorem is what lets us know that we cannot, in general, prove the existence of a (set) model of ZFC within ZFC itself. This is a fundamental obstruction to naive methods of proving relative consistency results. We cannot show, for example, that the continuum hypothesis is unprovable in ZFC by constructing a set model of ZFC where CH fails using methods that themselves can be formalized in ZFC. Philosophically, this says we should not be surprised that the relative consistency results that we do have require methods that cannot be formalized within ZFC.

Second, there are some theorems (perhaps less well known) that leverage the second incompleteness theorem to prove the existence of special kinds of models. These are mathematical results, not philosophical ones.

Theorem (Harvey Friedman). Let $S$ be an effective theory of second-order arithmetic that contains the theory ACA0. If there is a countable ω-model of $S$, then there is a countable $\omega$-model of $S$ + "there is no countable $\omega$-model of $S$."

The proof proceeds by showing that, if the conclusion fails, a certain effective theory obtained from $S$ is consistent and proves its own consistency. The type of model constructed by the theorem is useful for proving that certain systems of second-order arithmetic are not the same.

• I thought that Cohen's proof is formalizable in $ZFC$ in the form "if $ZFC$ is consistent, then $ZFC+\lnot CH$ is consistent". Sep 9, 2010 at 17:36
• Nice example! That's also what I was pointing to in my comment to the question. If you manage to carry out a consistency proof in a setting where you shouldn't be able to (by the 2nd incompleteness theorem), then you have a contradiction - which is valuable information about your hypotheses. Sep 9, 2010 at 17:37
• Carl, Is the proof of Harvey's result basically a use of $\Sigma^1_1$ absoluteness? I've proved versions of this in class for stronger theories, so perhaps I'm overlooking some technicality at the level of second order arithmetic. Sep 9, 2010 at 18:13
• @Kaveh: In my terminology, that approach proves the consistency of "ZFC + X" in the stronger theory ZFC + Con(ZFC). Sep 9, 2010 at 19:49
• @Andres: the proof does use the downward absoluteness of $\Pi^1_1$ formulas. There is a proof in Simpson's book on second-order arithmetic if you're interested in looking it up. The reason ACAo is needed is to reason about the satisfaction predicate of a countable $\omega$-model coded as a real. Strangely, every $\omega$-model of WKLo does contain a real that codes a countable $\omega$-model of WKLo, so the assumption of ACAo isn't trivial. Sep 9, 2010 at 19:57

While it's not directly a philosophical benefit, the Second Incompleteness Theorem is quite useful for giving concrete unprovability results: if we want to prove that theory T does not prove theorem X, it suffices to show that X implies the consistency of T. For instance, Harvey Friedman has a number of results showing that some theorem implies the well-foundedness of some ordinal notation, where the ordinal notation, in turn, is known to imply the consistency (indeed, 1-consistency) of the theory.

John H Conway proves and discusses the incompleteness theorem is his badass wolf prize lectures: http://www.math.princeton.edu/facultypapers/Conway/ Anyone who hasn't seen these talks is missing out.

• On a Mac, I'm able to play the video of these lectures using the free software VLC: videolan.org/vlc Sep 10, 2010 at 0:43

It is an open question whether what I have called Hilbert's ultrafinitist program is possible, that is whether a natural base theory can prove the consistency of natural stronger theories. Please see

Is an ultrafinitist Hilbert's program doomed?

So in this sense the Second Incompleteness Theorem is not redundant: there could be natural theories which prove natural stronger theories consistent.

In any case I'm of the opinion that proving self-consistency is a good test for a theory; that is, if a theory can't even prove its own consistency, that is a good reason not to accept the theory.

There is another nice consequence of the Goedel first incompleteness theorem. Indeed by proving that there exists an undecidable sentence, the theorem is offering a formal proof of the consistency of ZFC (if it were not consistent then it would prove whatever). The only problem is that it is doing so inside ZFC, so the proof is not really worth because it would carry on also if ZFC were inconsistent.

I think this is also related to your sentence "a mainstream opinion in mathematics ... is that we believe that there is no problem with ZFC".

• The consistency of the theory is a hypothesis in the incompleteness theorems; they don't establish the consistency themselves. Sep 10, 2010 at 11:22