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)?
Best Answer
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).