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

  • $\begingroup$ 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. $\endgroup$ Commented Mar 29, 2022 at 12:34
  • 1
    $\begingroup$ Related. $\endgroup$
    – Git Gud
    Commented Mar 29, 2022 at 12:35
  • $\begingroup$ 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. $\endgroup$
    – Peter
    Commented Mar 29, 2022 at 12:38
  • $\begingroup$ 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. $\endgroup$
    – Peter
    Commented Mar 29, 2022 at 12:40
  • 1
    $\begingroup$ 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. $\endgroup$
    – Peter
    Commented Mar 29, 2022 at 12:51

1 Answer 1


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .