# What's the big deal with Gödel's second incompleteness theorem?

Edit: My question is specifically about Gödel's second incompleteness theorem. I get the significance of his first incompleteness theorem, which is of course completely amazing.

According to the Wikipedia entry on Gödel's second incompleteness theorem, "the broadly accepted natural language statement of the theorem is" as follows.

For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.

I accept that the above theorem is mathematically useful (say, for proving the inconsistency of a system). But why is it philosophically interesting? Assume it was false. Suppose there was a theory that was consistent, and also included the basic arithmetical truths that Gödel's theorem speaks of, and could also prove its own consistency. For concreteness, suppose ZFC could do this.

Well, so what? It's clearly circular.

Now I'm not doubting the mathematical usefulness of Gödel's theorem. But my question is, on a philosophical level, what's all the commotion about?

• This belongs on philosophy.SE, voting to close as off topic. (I also flagged for moderator attention to have this migrated.) – Asaf Karagila Feb 5 '13 at 13:47
• Don't you think your question is off topic here, in particular since you say you're not questioning anything about mathematics but about philosophy...? – DonAntonio Feb 5 '13 at 13:47
• I've answered almost the same question before. – Henning Makholm Feb 5 '13 at 13:48
• Migrating to philosophy. – Willie Wong Feb 5 '13 at 14:58
• So far my answer is the only one that points out an error in reasoning in the posted question. – Michael Hardy Feb 5 '13 at 20:43

You observe, correctly, that just because a formal system S "asserts" its own consistency — by means of a proof which, in a meta-language M, is isomorphic to a proof of consistency of S — does not mean that you should therefore trust S to be consistent. Any inconsistent system which is rich enough to admit Gödel numbering (or an equivalent technique), and which has an explosive implication (so that everything follows from a falsehood), is able to prove its own consistency; although it would be interesting to know whether or not it allows you to derive "consistency claims" without passing through blatant contradictions of the form A & ¬A to do so.

The big deal with Gödel's Second Incompleteness theorem is that the only formal systems which can "prove" their own consistency via encoding in Peano Arithmetic (or an equivalent system) — and which is also able to prove that addition and multiplication are total functions — are in fact inconsistent. Even if we knew from first principles that we could not rely on internally proven consistency claims, there is the ironic twist that in fact such "proofs of consistency" are in fact proofs for precisely the opposite.

What this really means is that consistency is a bit of a chimeral property of a formal system to have. We are denied even the conceit of self-verifiability in totalizing formal systems. You can of course prove that a formal system S is consistent in another formal system M — but then why should you accept that M is consistent? Proving it so in another system M' is just pushing the problem away a further step. The consequence is that consistency of a formal system is a fundamentally negative property: a failure to be able to exhibit a contradiction, in which case you can never be sure if it is really consistent, or if you just haven't realized how to produce a contradiction in the system.

In the end, Gödel's Second Incompleteness theorem says that unless (like Gödel himself) you believe that humans somehow have a sort of occult-ish access to timeless Platonic truth, mathematics is subject to the same epistemological limitations as the natural sciences, in which formal systems play the role of theories and the discovery of inconsistencies play the role of falsification.

• @ArthurFischer: hi! That's actually quite intriguing. I will have to take a close look at Willard's self-verifying system (in which, for the folks at home, multiplication is not provably a total function) to grok what's going on there. – Niel de Beaudrap Feb 5 '13 at 16:09
• My comment above was in reference to a comment correcting an earlier version of my post, which didn't account for the existence of a formal system as described in a post on MathOverflow about such systems of arithmetic. Gödel's Second Incompleteness theorem relies on certain properties of arithmetic which --- if a formal system cannot prove them --- is ipso facto exempt from Gödel's theorem. Of course, if the system is sufficiently different from Peano Arithmetic, it's not clear what the long-range implications are. – Niel de Beaudrap Feb 5 '13 at 16:18
• "In the end, Gödel's Second Incompleteness theorem says that... mathematics is subject to the same epistemological limitations as the natural sciences, in which formal systems play the role of theories and the discovery of inconsistencies play the role of falsification." I certainly agree with the conclusion, but how does Godel's second incompleteness theorem imply it? It seems to me the very nature of the axiomatic method implies it. You start with some assumptions, and use those assumptions to prove the consistency of other systems of assumptions. But if you're original assumptions were..... – goblin Feb 5 '13 at 21:50
• ...inconsistent, then your precious proof ultimately amounted to nothing. – goblin Feb 5 '13 at 21:51
• @user18921: indeed. Of course, people felt differently, perhaps because they thought that perhaps one could obtain very simple systems of axioms which were "manifestly" (i.e. could be trusted to be) consistent, and that one could then prove the consistency of other systems using it. This is a charicature of Hilbert's programme, of course. Gödel proved that you can't hope to do such a bootstrapping proof of consistency, from something which is simpler: any such attempt will fail. And so positivism, which is the most prevalent social attitude to mathematics, is refuted. – Niel de Beaudrap Feb 6 '13 at 0:37

The other answers miss something important. The real impact of the Second Theorem isn't in the limitations it places on a theory's proving its own consistency. The key point is this. If a nice arithmetical theory T can't even prove itself to be consistent, it certainly can't prove the consistency of a richer theory T+ which extends T (since proving the richer theory is consistent, proves a cut-down part of it is consistent). Hence the fact that an arithmetic theory like PA can't prove its own consistency means we can't use 'safe' reasoning of the kind we can encode in ordinary arithmetic to prove that other more 'risky' mathematical theories are in good shape.

For example, we can't use unproblematic arithmetical reasoning to convince ourselves of the consistency of set theory (with its postulation of a universe of wildly infinite sets).

And that is a very interesting result, for it seems to sabotage what is called Hilbert's Programme, which is precisely the project of trying to defend the wilder reaches of infinitistic mathematics by giving consistency proofs which use only 'safe' methods. (For a great deal more about this, see my Gödel book!)

• see my comments under Niel de Beaudrap's answer. EDIT: If you're interesed, of course. – goblin Feb 6 '13 at 2:31
• On second thoughts, don't worry about my other comments. Tell me, is the following what you mean: suppose I wish to prove that ConA -> ConB in a metatheory. A simple approach would be to prove (in the language of A) a suitable interpretation of the statement ConB. What you're saying is that if A is sufficiently rich that Godel's second inconsistency theorem applies, then this simple approach cannot work. EDIT: So basically, we can still try to prove ConA -> ConB in the metatheory, but the aforementioned simple approach won't do it. – goblin Feb 6 '13 at 4:45
• I cannot edit the above comment, but it should read "Suppose I wish to prove that ConA -> ConB in a metatheory, where B is richer theory than A." – goblin Feb 6 '13 at 5:03
• @user18921 The point I take from Peter's post is that the significance of the second incompleteness theorem is that it puts a sort of upper bound on the strength of theories if they are to prove their own consistency. In particular, it shows us that a very weak theory capable of formulating a theory as weak as PA can't prove its own consistency. So, since any stronger theory would contain the necessary materials to perform the needed arithmetization of syntax (Godel Numbering) it would also fall victim to Godel's theorem and thus would be unable to establish its consistency. – Dennis Feb 6 '13 at 18:32
• @user18921 The reference to Hibert's Programme is about Hilbert's attempts to found all of mathematics upon finitary mathematics. You can read about it at the SEP. Section 4 should be of special interest to you as it discusses the implications of incompleteness for the Program. Apparently there is controversy over which of the two theorems dealt the death-blow to Hilbert's Program. – Dennis Feb 6 '13 at 18:39

An additional gloss to Peter Smiths answer that a weaker system cannot prove a stronger system consistency, is that a system incomparable to another may prove it consistent.

For example, in Gentzen's proof of the consistency of PA (Peano Arithmatic) he uses PRA (Primitive Recursive Arithmatic) and quantifier free transinfinite induction. It is not stronger than first order arithmetic (it can't prove induction), nor is it weaker (it can prove consistency of PA which PA can't).

I know that after learning about Gödel's incompleteness theorem, it came as a surprise to me that there could be a proof of PA's consistency.

• How are you defining incomparable? If you're saying that "A is incomparable to B" means "neither Con(A) implies Con(B), nor does Con(B) imply Con(A)," then I don't understand how theory A can prove the consistency of an incomparable theory B. – goblin Feb 6 '13 at 10:00
• @user18921: I don't understand the details of the proof - so I can't enlighten you as to exactly how Gentzen manages this. But I do know its accepted by the mathematical community, and I can also see that the claim of incomparability stands as I've indicated above. – Mozibur Ullah Feb 7 '13 at 0:51

Here's what I wrote on circularity, but didn't post (I am really just agreeing with what Michael Hardy said in more detail.. this should be a comment but it's too long):

I think it's a really good point that proving a mathematical theory (like PA or ZFC) consistent using the theory itself is circular. If the theory did happen to be inconsistent, it could prove its own consistency! So the mere existence of a consistency proof doesn't tell you anything: The real value in a consistency proof is telling you how strong an induction principle (or how big an infinite ordinal) you need to show that there isn't a proof of false: For example we need $\omega^2$ for the simple typed lambda calculus (which corresponds to a very simple constructive propositional logic), $\epsilon_0$ for PA.

• You're "really good point" is confused. If the mere fact that one can prove consistency of a system within the system is cited as evidence that it's consistent, that's circular reasoning. But such a proof gives you more than that: you know the details of the specific proof. In particular, you know which of the axioms of the system it relies on. If you use the first three of the system's axioms to prove consistency of the whole system of 20 axioms, and therefore conclude that the whole system is consistent because you were already confident of the consistency of the first three, then..... – Michael Hardy Feb 5 '13 at 20:39
• ....you are not reasoning circularly. But Gödels incompleteness result tells you that in certain kinds of cases, that cannot be done. – Michael Hardy Feb 5 '13 at 20:40
• @MichaelHardy, I don't understand your remark 'You're "really good point" is confused' at all. You just repeated back exactly what I said except you focus on "a subset of the axioms" rather than proof theoretic ordinals. As I already said we are in agreement, I only posted my text because I think people were confused about the meaning of your comment and downvoted you because of that. – user3085 Feb 5 '13 at 20:43
• Your first sentence says "proving a mathematical theory (like PA or ZFC) consistent using the theory itself is circular." That is at best unclear. It's not circular. Knowing only that there is such a proof, without knowing any of its details, and concluding consistency, would be circular. But "proving [it] consistent using the theory itself" doesn't mean that. You wouldn't know only that there is such a proof; you'd know specifically what the proof is. – Michael Hardy Feb 5 '13 at 20:46
• @user58512 You're saying that if such a proof of the consistency of T existed within T, then we'd be able to conclude that, "If T is consistent, then it's proof theoretic ordinal is at least.... WHAT?" Can you clarify? – goblin Feb 5 '13 at 21:40

Gödel showed that truth and provability don't necessarily coincide. In a certain sense, he also showed that not every statement is necessarily either meaningless or either true or false. Already Aristotle envisioned that this might be the case for statements about the future.

The question whether mathematics is consistent is interesting, but so is the question: "Are mathematical models fundamentally different from the real world around us, or is it possible to approximate by mathematical models the important aspects of the world around us which we want to investigate?"

Once we believed that the world around us is deterministic, and that mathematics itself is "even more" deterministic. We learned later that the world around us is not as deterministic as we thought, and Gödel's incompleteness theorems taught us that mathematics is also less deterministic than we expected.

I once asked myself: "How to model non-existence (or not-yet existence) mathematically?". If I recall correctly, I was thinking about questions of measurability at that time. However, the point remains that a consistent and finitistic mathematic would probably be too limited to reflect the infinite, unbounded and inconsistent real world sufficiently accurate.

• You write: "Gödel showed that truth and provability don't necessarily coincide." Firstly, this is slightly inaccurate. We always knew that the truth and provability of sentences don't necessarily coincide. For instance, if my system for talking about the natural numbers consists of only one axiom, which postules the existence of an element, well clearly not all that is true about the natural numbers can be proved in this system.... – goblin Feb 6 '13 at 2:37
• ...What Godel ACTUALLY showed is that, contrary to what we'd always hoped, truth and provability can't be made to coincide; no matter how many finitely many axioms we add, it's not enough. In fact, even if we allow for a semidecision procedure to specify our axioms, IT'S STILL NOT ENOUGH. Pretty amazing. However, that's Godel's FIRST incompleteness theorem. My question is, what's the significance of his SECOND? – goblin Feb 6 '13 at 2:38
• This does seem to be about Gödel's first incompleteness theorem rather than his second incompleteness theorem. The latter is what the question was about. – Michael Hardy Feb 6 '13 at 3:49
• It's true that this answer isn't specifically about the SECOND incompleteness theorem. It tries to explain why incompleteness and undefinability theorems in general have implications for the philosophy of mathematics (especially for the relation between mathematics and the real world). While writing, I asked myself how much this answer is only concerned with finitistic mathematical systems (and implicit compactness properties), and whether the actual incompleteness theorems are really limited to the finitistic case. Also, the concept of a "real world" might have needed clarification. – Thomas Klimpel Feb 6 '13 at 7:39
• @user18921 I can remove this answer, if you think it doesn't address your question. I agree that it doesn't even try to refer to the SECOND incompleteness theorem, but I think that it isn't limited to the first incompleteness theorem either. It just says that the incompleteness theorems are an important contribution to better understand the relationship between mathematical models and the "real world". – Thomas Klimpel Feb 6 '13 at 7:48

It's not circular!

If the mere fact that one can prove consistency of a system within the system is cited as evidence that it's consistent, that is circular reasoning. But such a proof gives you more than that: you know the details of the specific proof. In particular, you know which of the axioms of the system it relies on. If you use the first three of the system's axioms to prove consistency of the whole system of 20 axioms (including those first three), and therefore conclude that the whole system is consistent because you were already confident of the consistency of the first three, then you are not reasoning circularly. But Gödels incompleteness result tells you that in certain kinds of cases, that cannot be done

• Michael, can you clarify a little? I sort of get the "vibe" of what you're saying, but the details aren't transparent to me. – goblin Feb 6 '13 at 2:40
• Say you have a set of 20 axioms and for some good reason you believe that the set of the first three of those 20 is consistent. If you then write a proof of consistency of the set of all 20, relying only on the first three in that proof, then that's a proof of the consistency of all 20 within the system whose consistency you're proving. And it's not circular. If that doesn't clarify what I'm saying, then probably you need to clarify your questions. – Michael Hardy Feb 6 '13 at 3:48
• What language is the proof of consistency written in? The language of the 3 axioms, or a metalanguage? – goblin Feb 6 '13 at 4:07
• It's in the same language as the three axioms, not a metalanguage. Otherwise it wouldn't be within the system. – Michael Hardy Feb 6 '13 at 15:59