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

• PA can’t prove its consistency, but actually the real goal was to show using finitary reasoning that PA is consistent, Goedel showed this to be impossible, by the second incompleteness theorem. Mar 29, 2022 at 12:34
• Mar 29, 2022 at 12:35
• Gentzen found a work around , but consider that this is still no surefire proof of the consistency of the peano axioms since it uses transfinite induction. In fact, there is no guarantee for the consistency of any theory at least as powerful as the peano axioms. Why this is important ? Because an inconsistent theory is utterly useless since it can prove every (even false) statement. Mar 29, 2022 at 12:38
• PA cannot prove the consistency of ZFC since it would then in particular prove the consistency of PA (which Goedel proved to be impossible). Hence it does not help to use a weaker theory completely contained in the stronger theory. Mar 29, 2022 at 12:40
• Also note that you do not need worry about a possible breakdown of math. The discovery of Russel's paradox did not lead to a breakdown of math , and a possible future detection of another inconsistency of ZFC will not "destroy" math either. Mar 29, 2022 at 12:51