MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

For simplicity, let me pick a particular instance of G\"odel'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 inacessible cardinal is not provable in ZFC"? In other words, does this reduce the Second Incompeteness 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)?

share|cite|improve this question
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.) – John Stillwell Sep 9 '10 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. – Andrés E. Caicedo Sep 9 '10 at 16:49
@Stefan: Do you think the first theorem already invalidates Hilbert's program? – Andrés E. Caicedo Sep 9 '10 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? – Peter Arndt Sep 9 '10 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. – Stefan Geschke Sep 9 '10 at 19:59
up vote 27 down vote accepted

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"odel) have been useful, and I think this is what Hilbert was hoping for. G"odel's second incompleteness theorem tells us that this sort of thing can't happen (unless even the more reliable system is inconsistent).

share|cite|improve this answer

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

share|cite|improve this answer

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.

share|cite|improve this answer
I thought that Cohen's proof is formalizable in $ZFC$ in the form "if $ZFC$ is consistent, then $ZFC+\lnot CH$ is consistent". – Kaveh Sep 9 '10 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. – Peter Arndt Sep 9 '10 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. – Andrés E. Caicedo Sep 9 '10 at 18:13
@Kaveh: In my terminology, that approach proves the consistency of "ZFC + X" in the stronger theory ZFC + Con(ZFC). – Carl Mummert Sep 9 '10 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. – Carl Mummert Sep 9 '10 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.

share|cite|improve this answer

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.

share|cite|improve this answer

John H Conway proves and discusses the incompleteness theorem is his badass wolf prize lectures: Anyone who hasn't seen these talks is missing out.

share|cite|improve this answer
On a Mac, I'm able to play the video of these lectures using the free software VLC: – Dan Ramras Sep 10 '10 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.

share|cite|improve this answer

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

share|cite|improve this answer
The consistency of the theory is a hypothesis in the incompleteness theorems; they don't establish the consistency themselves. – Carl Mummert Sep 10 '10 at 11:22

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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