Question

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 was 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 was 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)?

Answer 1

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

Answer 2

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

Answer 3

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 ACA₀. 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.

Answer 4

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.

Answer 5

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.

Answer 6

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