# Proof of Gödel's Incompleteness Theorem by modal logic

I watched Undefined Behavior's videos (on YouTube) regarding Gödel's Incompleteness Theorem, and the last video slightly confuses me.

Let $$\square P$$ denote "There is a proof of the statement $$P$$." In the first video, he asserts the classical logic, and the following axiom:

$$\square P \implies P$$

That is, axiom T.

In the second video, he proves a weakened version of Gödel's First Incompleteness Theorem. "Every axiom system is either incomplete or unsound." That is:

$$\exists P \neg(\square P \lor \square \neg P) \lor \exists Q (Q \land \square \neg Q)$$

Where $$P$$ and $$Q$$ are statements.

In the last video, he proves Gödel's First Incompleteness Theorem, that is:

$$\neg \exists Q (\square Q \land \square \neg Q) \to \exists P \neg(\square P \lor \square \neg P)$$

And then he proves Gödel's Second Incompleteness Theorem. It goes:

Assume math is consistent, and denote it by $$M$$. Then there exists a statement $$S$$ ("Mr. Smith loops") such that $$\neg(\square S \lor \square \neg S)$$. Yet $$S$$ is actually true. In other words, $$M \to \neg(\square S \lor \square \neg S)$$ and $$M \to S$$. If $$\square M$$ were true, we will have $$\neg \square S$$ and $$\square S$$. This is contradiction, thus $$\neg \square M$$.

I'm slightly convinced, but I don't understand it formally.

Can anyone formalize the last proof? Or is the video wrong?

Edit I rewrote the answer, to tailor more to the actual arguments given in the video rather than the usual textbook proofs.

The argument is basically correct, but requires some elaborate technical arguments to make rigorous. The key point was at 4:40 in the video, where they say "if we formalize this idea...". This is where all the details were glossed over.

For clarity (and so people who don't want to watch the videos can follow the answer), I'll reiterate the argument for the first incompleteness theorem. Let $$T$$ be a "nice theory".$$^*$$ We write down a program

def Smith(M):
for p in proofs_T():
if p proves M(M) loops:
return
if p proves M(M) halts:
loop()


where proofs_T() is a generator of an effective enumeration of valid proofs from our theory $$T.$$ Let $$S$$ be the statement "Smith(Smith) loops". Then we see that if $$T$$ is consistent then it can neither prove $$S$$ nor $$\lnot S.$$

• If $$T\vdash S,$$ then when we run Smith(Smith), it will eventually find the proof of this and halt (since $$T$$ is consistent we won't get beaten to the punch by a proof of $$\lnot S$$). Thus Smith(Smith) halts. But we have assume $$T$$ is sufficiently strong that if a program halts, $$T$$ can always prove this, so $$T\vdash\lnot S$$ and so $$T$$ is inconsistent after all.
• If $$T\vdash\lnot S$$ then as in the other case, when we run Smith(Smith) it will find the proof and call loop(). But then, again due to our strength assumptions, $$T$$ can prove Smith(Smith) will get to this point where we call loop() so $$T\vdash S$$ and $$T$$ is inconsistent after all.

Thus we have shown the first incompleteness theorem.

If $$T$$ is consistent then $$T\nvdash S$$ and $$T\nvdash \lnot S.$$

Now for the part you are asking about. The argument goes like this: We claim that if $$S$$ is unprovable, then it is true. The argument is that if $$S$$ were false then Smith(Smith) halts, but looking at the program, the only way this can happen is if we find a proof that Smith(Smith) loops, and thus $$T\vdash S.$$ Thus, taking the contrapositive, $$\lnot\square_T S\to S$$.

Then, the first incompleteness theorem says that $$\operatorname{Con}(T)\to \lnot\square_T S,$$ so stringing this together with the previous result implies $$\operatorname{Con}(T)\to S.$$ And thus if we could prove $$\operatorname{Con}(T)$$ then we could prove $$S,$$ which contradicts the first theorem (assuming $$T$$ is consistent). Thus we have that if $$T$$ is consistent then it cannot prove $$\operatorname{Con}(T).$$

But this got pretty muddy and we were vague about some of the details as to who was proving what, so lets go back through the details carefully. Let's look at the first piece first where $$\lnot \square_T S\to S$$ was shown. This was a simple analysis of the program where we just found the only place it could halt and concluded that this meant a certain proof needed to exist. And so this argument can be carried out in $$T,$$ so we have $$T\vdash \lnot \square_T S\to S.$$

It's the other part that makes things difficult. Our proof of the first incompleteness theorem was done in the metatheory, not in $$T,$$ using some pretty sophisticated analysis of provability, and so it's not obvious that we actually have $$T\vdash \operatorname{Con}(T)\to \lnot\square_T S.$$ But "if we can formalize" the proof in $$T$$, then we're good to go, since then we have if $$T\vdash\operatorname{Con}(T),$$ then $$T\vdash S,$$ so is inconsistent by the first theorem.

But it turns out that rigorously showing that $$T\vdash \operatorname{Con}(T)\to \lnot \square_T S$$ is extremely technical, to the point that nearly every introductory textbook punts on this part of the argument$$^{**}$$. The usual approach is to reduce the problem to establishing a few metalogical properties of the proof predicate, known as derivability conditions. Then we can show that if the derivability conditions hold, this gives us the necessary strength to formalize the proof (actually, usually the proof is not formalized directly and rather a shortcut is taken through Löb's theorem, but that's not really important). The tedious and technical part that the books punt on is showing that the derivability conditions hold in sufficiently strong theories.$$^{***}$$

$$^*$$Let's say a computably enumerable theory that can decide every (encoded) statement that says a program is at a given line after a given number of steps, as well as every statement that says a given proof is a valid proof of a given statement. That $$T$$ extends PA certainly suffices.

$$^{**}$$The standard approach uses a somewhat different statement $$S$$ and has a somewhat different proof of the relevant parts of the first incompleteness theorem that we need to formalize, but the idea here is the same. On another note, I don't mean to give the impression that the proof in the video of the first incompleteness theorem is completely rigorous by contrast. Like for the second, it is a pretty accurate sketch of an argument but there are a lot of technical details omitted (in particular we need to show we can represent these computer programs in our theory, and represent the idea of proofs, amongst other things). But by contrast, the technical details behind the first theorem are usually shown more-or-less in full in an introductory treatment. This is because even though they are tedious in places, they are less technical then proving all the derivability conditions, and more importantly they are of independent interest and utility.

$$^{***}$$ As a minor technical point, what's "sufficiently strong" for the derivability conditions is actually somewhat stronger than Robinson arithmetic, which is the natural notion of "sufficiently strong" that suffices for the first incompleteness theorem. Incidentally, even though the derivability conditions fail, the second theorem can be proven for Robinson arithmetic through other means.