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