Why is proving system consistency a problem?

Question

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?

Answer 1

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.

Answer 2

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)]

    $\bot$.

  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.)