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