Interpretation of the Second Incompleteness Theorem 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)?
 A: 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. 
A: 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.
A: 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).
A: 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.)
A: 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.
A: 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. 
A: 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".
A: 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.
