I have problems understanding Gödel's incompleteness theorem. I presume I have a misunderstanding of some phrase or I have to look closer at the meaning of some detail.

Gödel's second incompleteness theorem states that in a system which is free of contradictions, this absence of contradictions is neither provable nor refutable.

If we would find a contradiction, then we would have refuted the absence of contradictions. Gödel's theorem states that this is impossible. So we will never encounter a contradiction. Doesn't that mean that no contradiction exists? (If one existed, we could encounter it.) So this seems to be a proof that no contradiction exists. Thus, we proved the absence of contradictions, which contradicts the second incompleteness theorem.

This is a contradiction which I can't solve.

  • 3
    $\begingroup$ Note that the theorem statement is "if a system is free of contradictions...", and thus it says absolutely nothing about the case when a system has contradictions. $\endgroup$ – Wojowu Jan 13 '15 at 10:16
  • 2
    $\begingroup$ In fact, I do not understand the concept of 'system' in this context and thus I can't tell when I'm inside and when outside of a system. $\endgroup$ – Daniel S. Jan 13 '15 at 10:42
  • 1
    $\begingroup$ A "system" referenced in the theorem is so called formal theory, which is just a collection of axioms and deduction rules which allows us to derive theorems. $\endgroup$ – Wojowu Jan 13 '15 at 11:03
  • 1
    $\begingroup$ The the question in the title, no. It does not contradict itself. $\endgroup$ – Asaf Karagila Aug 11 '15 at 7:11
  • 1
    $\begingroup$ You might want to take a look at the book "Gödel's proof" by Nagel & Newman. It may not be perfect, but it does go a long way in putting Gödel's work into context. Particularly the inside/outside the system dichotomy is well illustrated, which is central to understanding the proof. $\endgroup$ – Fasermaler Aug 25 '15 at 12:34

I know this is late, but your comment about "inside" and "outside" is the crux. Basically "proof" is always relative to the proof system.

Define a formal system as useful iff it has a proof verifier program. Godel effectively showed that there is a program that, given the proof verifier for any useful formal system $S$, will always output a sentence $Con(S)$ over PA, such that ( $\mathbb{N} \vDash Con(S)$ ) iff S is consistent. Note that this can only be stated and proven in a meta-system that is strong enough to effectively reason about programs and halting behaviour, which includes 'knowing' $\mathbb{N}$ as some 'structure' that satisfies PA. Godel-Rosser's theorem is that if $S$ is a consistent useful formal system that interprets arithmetic, then $S$ does not prove the interpretation of $Con(S)$. See this post about the specific case where $S$ is an extension of PA, and be careful not the make the same mistake as Robert Israel.

For more details and a bit on provability logic, see this post. The incompleteness theorem is actually far more general than most textbooks set out, because it applies to any useful formal system as I've defined above, including non-classical logics, yet-to-be-discovered logics, ... For the general case we must define what "interprets arithmetic" means, which I do in this post before proving the general incompleteness theorem using a different proof from Rosser's. And for a more precise calibration of what is "strong enough" for the meta-system, see this post.


I'm a bit of a novice here, but I think this may help.

(Note: I'm using Peano Arithmetic (PA) here but you can replace it with whatever theory you're talking about the Second Incompletness Theorem (G2) with respect to.)


  1. A theorem of PA is defined to be a sentence in PA's language (i.e. a string of PA's symbols satisfying certain conditions) which can be concluded from the axioms of PA by finite applications of the rules of inference of PA (those of first-order logic).
    • If S is a theorem of PA, we say PA proves S (symbolically, PA$\vdash$S). Otherwise, we say PA does not prove S (symbolically, PA$\nvdash$S). With this notation, we can state G2 as PA$\nvdash$ConPA].
  2. "PA is consistent" means there is no pair of theorems of PA which are each other's negation, and "inconsistent" means not consistent.

Clarifying Key Notions

There is a statement (let us call it ConPA) in the language of PA (i.e. ConPA is a string of symbols that can actually be written out--although it takes pages), that is true in the standard model of PA iff PA is consistent (and so its negation is true iff PA is inconsistent). Crucially, by the previous sentence, I do not mean PA can prove ConPA iff PA is consistent, and I do not mean ConPA is true iff PA can prove ConPA. I mean ConPA is true iff PA is consistent. (When people talk about whether PA can prove its own consistency, all they are talking about is whether PA proves ConPA.) G2 is this: "if PA is consistent, PA does not prove ConPA i.e. PA$\nvdash$ConPA." Note that G2 is not a theorem of PA. As I've presented it here, G2 is just a general fact about the world, and is not a sentence (let alone a theorem) of any formal theory (although, as I recall, it can be sort of paraphrased and proven in some formal theories in much the same way that, in PA, ConPA paraphrases "PA is consistent" although PA doesn't prove ConPA). It is a direct consequence of the soundness of PA (the fact the axioms of PA are true and the rules of first-order logic are truth preserving) that if PA is consistent then PA$\nvdash \neg$ConPA--this is not a consequence of G2 as far as I can see.

Actually Answering the Question

If I understand the question correctly, it expresses concern that it follows from G2 that PA (or any formal theory) is consistent since if it wasn't there would be a contradiction in it and that would mean PA would prove its own inconsistency, which is just what G2 says it cannot do--a putative contradiction itself.

Various issues with that: G2 doesn't say that PA can't prove its own inconsistency; it says that if PA is consistent, it can't prove its own consistency--an inconsistent theory proves everything in its language. While it does follow from the soundness of PA (which is a fact) that if PA is consistent then PA doesn't prove its own inconsistency (and maybe this is sometimes considered part of G2), this does not show that PA does not prove its own inconsistency because we don't know for sure that PA is consistent. Now you might be concerned that under the assumption that PA is consistent, the fact (the conclusion of G2) that it cannot prove its consistency (that is, prove ConPA) would mean that PA isn't consistent and this would contradict G2. But this implication (if it doesn't prove a sentence S, then S is false) would only hold if PA were complete and it is not complete as the first incompleteness theorem shows.

  • 1
    $\begingroup$ Note that any theory that can express and prove the soundness of PA can also prove Con(PA). So unless we are also assuming one of those theories is consistent, it may be the case that PA is consistent and PA proves ~Con(PA). But this would mean that ZFC is inconsistent. $\endgroup$ – Dan Brumleve Sep 4 '15 at 0:13

It does not state that the absence of contradictions is not refutable. However "Gödel's second incompleteness theorem states that in a system which is free of contradictions, this absence of contradictions is not provable" is accurate.

It may be the case that ZFC for example is consistent and also that "ZFC is inconsistent" is a theorem of ZFC.

  • $\begingroup$ It's already covered by the definition of the system: Refuting the absence is the same as proving the existence. But the system is free of contradictions by definition, so it is impossible to prove the existence of a contradiction. As we said, that's the same as when it's impossible to refute the absence, i.e. the absence is not refutable. $\endgroup$ – Daniel S. Sep 3 '15 at 16:22
  • $\begingroup$ "But the system is free of contradictions by definition, so it is impossible to prove the existence of a contradiction." Try to distinguish "the system proves a contradiction" from "the system proves that the system proves a contradiction". The former is ruled out by the assumption that the system is consistent, but not the latter. $\endgroup$ – Dan Brumleve Sep 3 '15 at 21:24
  • $\begingroup$ Also consider adding to a consistent theory a new axiom claiming the inconsistency of the original theory. The resulting theory is also consistent, since the original theory cannot contradict the new axiom. Furthermore the resulting theory proves its own inconsistency since it assumes the inconsistency of a subtheory. $\endgroup$ – Dan Brumleve Sep 3 '15 at 21:26
  • $\begingroup$ I have the feeling there is still a part which I don't understand. Here I would think that then again, the resulting theory is not free of contradictions, and then the theorem doesn't say anything about the resulting theory, because it gives a statement only about theories which are consistent. $\endgroup$ – Daniel S. Sep 4 '15 at 12:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.