Why was it important for Peano arithmetic to prove ITS OWN consistency? A paraphrase of Gödel's Second Incompleteness Theorem into non-technical language states that, if a formal system is powerful enough to express Peano arithmetic, that system is unable to prove its own consistency.
This result is often - though not universally - taken to be the final nail in the coffin of  attempts to prove that arithematic is consistent. What I don't fully understand is: Why did the proof of consistency have to be made from within arithmetic? I think I have an inkling of the reason. Perhaps it has to do with fact that, if the consistency of arithmetic was proved within another system, the consistency of that system would also have to be proved, potentially leading to an infinite regress? But I can't quite answer my own objection: Could we not prove the consistency of arithmetic from a simpler formal system, the proof of the consistency of which might be more straightforward? Is there some result which states that, if one can prove the consistency of formal system $A$ from within formal system $B$, then $B$ must be at least as powerful as $A$?
 A: Perhaps the most succinct answer is given by Hilbert in his article Über das Unendliche (On the Infinite):

There is just one condition, albeit an absolutely necessary one,
connected with the method of ideal elements. That condition is a proof
of consistency, for the extension of a domain by the addition of ideal
elements is legitimate only if the extension does not cause
contradictions to appear in the old, narrower domain, or, in other
words, only if the relations that obtain among the old structures when
the ideal structures are deleted are always valid in the old domain.
[Philosophy of Mathematics: Selected Readings edited by P.
Benacerraf and H. Putnam, 2nd edition, Cambridge University Press,
1983, p. 199]

Demonstration of self-consistency, together with completeness, is an indispensable requirement of Hilbert's programme on the whole of mathematics. Indeed, the fundamental roles of these two notions reasonably follow from his formalist vision of mathematics, that is, to put the point overly simply, an architecture that would describe mathematical objects and relations in their utmost generality, hence, in ideally abstract fashion.
Since the envisioned formal system would be bereft of any objects and relations that endow mathematical symbolism with meaning, thus traditionally serves as a guiding content against fallacies and defects, the system itself has to guide itself abiding by metamathematical principles and values. Gödel's incompleteness theorems show that both pillars of Hilbert's programme are unrealisable.
Of course, this could be an end to Hilbert's programme, but it is an important research topic to see to what extent a formal system accomplish within itself.
