Interpretation of the Second Incompleteness Theorem

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


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


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.