I'm trying to understand Godel's second incompleteness theorem, which by my understanding is equivalent to, "An axiomatic system [with certain complexity and soundness properties] $F$ cannot prove its own consistency, i.e. $F⊬(F ⊬ 0=1)$" as a specific example following on from the first incompleteness theorem stating, "There is some syntatically valid sentence that $F$ cannot prove either true or false."

I understand that consistency is a ludicrously strong statement, since it's effectively an assertion over a set of completely general, arbitararily complex sentences and because of that, I wouldn't expect it to be provable to begin with. However, the 2IT says that this statement's not merely practically unreasonable, but directly implies a contradiction. (Or has some other self-defeating implication)

So, what contradiction can be derived from the assumption that a sound theory can prove that it itself is consistent, and how?


Take any useful formal system $S$, namely one that has decidable proof validity and uniformly interprets arithmetic (see the latter section of this post for the precise definition). $ \def\eq{\leftrightarrow} \def\box{\square} $

Then $S$ satisfies the Hilbert-Bernays provability conditions and the fixed point theorem (see the linked post), and hence we have both the internal and external forms of Lob's theorem (which arises from mimicking Curry's paradox in provability logic):

(L*) If $S \vdash □ P \to P$ then $S \vdash P$.

(L) $S \vdash □ ( □ P \to P ) \to □ P$.

From these applied to $P = \bot$ we immediately get Godel's second incompleteness theorem (in both external and internal form):

(GI*) If $S \nvdash \bot$ then $S \nvdash \neg □ \bot$.

(GI) $S \vdash \neg □ \bot \to \neg □ \neg □ \bot$.

To see where the contradiction comes from you can either trace through the proof of Lob's theorem and its instantiation to get the (external) first incompleteness theorem, or you can instantiate the proof from the beginning to get:

Let $P$ be a sentence such that $S \vdash P \eq \neg \box P$.

If $S \vdash \neg \box \bot$:

  Within $S$:

    $P \to \neg \box P$.   [from definition of $P$]

    $\box P \to \box \neg \box P$.   [by (D2)]

    If $\box P$:

      $\box \neg \box P$.

      $\box \box P$.   [by (D3) on last assumption]

      $\box \bot$.   [by (D2)]

      $\bot$.   [by outer assumption]

    Therefore $\neg \box P$.

    $P$.   [from definition of $P$]

    $\box P$.   [by (D1)]


  Therefore $S \vdash \bot$.

It is relatively easy to internalize the above proof of (GI*) within $S$ itself, which would give the internal form (GI).

Note also that this is for the usual definition of $\text{Con}(S) \equiv \neg \box_S \bot$. (There are possible alternatives.)

  • $\begingroup$ I have some problems with understanding syntax. Can you add a reference for that? $\endgroup$ – pqnet Dec 28 '18 at 11:50
  • $\begingroup$ @pqnet: Reference for what specifically? Have you read and understood the wikipedia article I linked to? $\endgroup$ – user21820 Dec 29 '18 at 16:07
  • $\begingroup$ Not exactly. I understood from en.wikipedia.org/wiki/Provability_logic that $□$ means "it is provable that" but still the meaning of $\vdash$ and $\bot$ are unclear, i assume $\neg$ is logical negation, I don't understand what the subscript mean in $□_S$ $\endgroup$ – pqnet Dec 30 '18 at 13:38
  • $\begingroup$ @pqnet: Hmm if you don't know what "¬" and "⊢" mean, then I'm afraid that you're going to have to learn basic first-order logic before you go anywhere near the incompleteness theorems. You can try Hannes' notes linked from this post, which should be enough if you are a mathematics major. If you don't have that kind of background, find me in this chat-room. $\endgroup$ – user21820 Dec 30 '18 at 15:57
  • $\begingroup$ As for notation, "$⬜_S$ was defined in the other post I linked to, and is the same notation in Peter Smith's "Godel without tears" (linked from the same post). Peter's book assumes you already have complete grasp of first-order logic up to the semantic-completeness and compactness theorems, but it is also the first book I learnt the conventional proof of Godel's theorems from. In my opinion, after the basics it may be more enlightening to take a more general yet shorter route as in this post, which explains the crux of incompleteness. $\endgroup$ – user21820 Dec 30 '18 at 16:16

No, the 2nd Incompleteness Theorem is just saying that "$F$ can't prove that $F$ can't prove that $0 = 1$". This is the same as saying that $F$ can't prove it's consistent - to say "$F$ is inconsistent" is to say "$F$ proves a contradiction", and from a contradiction you can prove anything at all, including $0 = 1$. So the statements "$F$ is inconsistent" and "$F \vdash 0 = 1$" are equivalent. What I mean is, the fact that we're now talking about a contradiction instead of consistency shouldn't be at all surprising here - they're the same thing.

As for which contradiction can be proven from a (sufficiently strong) sound theory that proves itself consistent: Any theory strong enough to handle arithmetic can prove Godel's Incompleteness Theorem. So this theory (let's call it $T$) "knows" that a sufficiently strong consistent theory cannot prove its own consistency. So $T$ proves that if $T$ is consistent, then $T$ cannot prove its own consistency. But if $T$ does prove its own consistency, it can prove that - it just has to supply the proof. So we have $T \vdash (Con(T) \implies T \nvdash Con(T))$ and $T \vdash T \vdash Con(T)$. So $T \vdash T \nvdash Con(T)$, because $T$ "knows" how implications work. Therefore $T \vdash (T \vdash Con(T) \wedge T \nvdash Con(T))$. That's a contradiction.

EDIT: The statement that $T$ "'knows' that a sufficiently strong consistent theory cannot prove its own consistency" isn't the First Incompleteness Theorem, it's the second. The Second Incompleteness Theorem states that if $T$ is "sufficiently strong" and consistent, then $T \nvdash Con(T)$. The interesting thing is that 2nd Incompleteness can be proven inside $PA$, so any sufficiently strong $T$ can actually prove that 2nd Incompleteness is true. The point is that if $T$ also proves that it itself is consistent, then it concludes that 2nd Incompleteness means it can't prove itself consistent.

  • $\begingroup$ Sorry but your answer is wrong. Specifically, your second paragraph. A counter-example: PA cannot prove that PA cannot prove Con(PA), unless PA itself is inconsistent! $\endgroup$ – user21820 Feb 4 '17 at 3:03
  • $\begingroup$ @user21820 Quite correct, thanks for pointing that out! I've made a minor edit that should address your concern. $\endgroup$ – Reese Feb 4 '17 at 3:39
  • $\begingroup$ I'm not quite sure now what you mean by "it can also prove that it itself is sound" since soundness is stronger than consistency. Your last few sentences are also arranged in a seemingly not logical fashion. Godel's incompleteness theorem gives your first claim $T \vdash (Con(T) \to T \nvdash Con(T))$, and (D3) gives your second claim $T \vdash ( T \vdash Con(T) )$. But if $T \vdash Con(T)$ then you simply get $T \vdash ( T \nvdash Con(T) )$ by ordinary modus ponens. $\endgroup$ – user21820 Feb 4 '17 at 3:49
  • $\begingroup$ Also you may be interested in looking at my post for the full proof of the incompleteness theorems via Lob's theorem, which is very elegant in my opinion. $\endgroup$ – user21820 Feb 4 '17 at 4:12
  • $\begingroup$ @user21820 Soundness is only stronger than consistency when evaluated externally. As far as $T$ is concerned, all it means for $T$ to be sound is "all of the axioms of $T$ are true", which $T$ can indeed prove. I only include it because OP referenced soundness; the theorem doesn't need it. And I don't understand your second complaint; you've written the same sentences I did, in almost exactly the same order, with exactly the same justifications. The only difference I see is that you're repeating $T \vdash Con(T)$ to justify the final step, whereas I just assumed the reader would recall it. $\endgroup$ – Reese Feb 4 '17 at 4:26

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.