Explaining Löb's theorem using Turing machines

A weird Turing machine

Consider a turing machine $M$ that compute the following algorithm:

Iterate over every every proof formalized in ZFC in lexicographic order.
if the proof is a proof that the turing machine $M$ halt's then halt.

The following construction is in fact possible, from Kleene's recursion theorem, Turing machines can compute functions based on their description.

Also it is important to note that the description of $M$ really describes a family of Turing machines, but what I'm going to state holds for any of them.

Is $M$ going to halt?

Another weird Turing machine

We can build another Turing machine $N$ computing the following algorithm:

Iterate over every every proof formalized in ZFC in lexicographic order.
if the proof is a proof that the turing machine $N$ halt's then $M$ halt's then halt.

The same things stated for $M$ also are true for $N$.

$M$ is going to halt

In ZFC we can construct a proof for the statement: $halt(N) \rightarrow halt(M)$

Proof:

From the fact that $N$ halts we can deduce the fact that it found a proof for the statement $halt(N) \rightarrow halt(M)$.

Given a proof for $halt(N)$ halts we can deduce that $halt(M)$ and indeed proving $halt(N) \rightarrow halt(M)$. $\blacksquare$

Clearly $N$ will find such proof and halt and by the same reasoning also $M$ will halt.

Löb's theorem

Löb's theorem roughly states that if a statement $P$ is provable then indeed it is also true, in modal logic we would write:

$$\square (\square P \rightarrow P) \rightarrow \square P$$

Where we read $\square \phi$ as $\phi$ is provable.

Proving Löb's theorem

It exists $\psi$ that satisfies $\vdash \psi \leftrightarrow (\square \psi \rightarrow P)$.
$\vdash \psi \rightarrow (\square \psi \rightarrow P)$, from 1.
$\vdash \square(\psi \rightarrow (\square \psi \rightarrow P))$, from 2.
$\vdash \square \psi \rightarrow \square (\square \psi \rightarrow P)$, from 3.
$\vdash \square(\square \psi \rightarrow P) \rightarrow (\square\square\psi \rightarrow \square P)$.
$\square \psi \rightarrow (\square \square \psi \rightarrow \square P)$, from 4 and 5.
$\square \psi \rightarrow \square\square \psi$, from 6.
$\square \psi \rightarrow \square P$, from 6 and 7.
Assume $\vdash \square P \rightarrow P$.
$\vdash \square \psi \rightarrow P$, from 8 and 9.
$\vdash (\square \psi \rightarrow P) \rightarrow \psi$, from 1.
$\psi$, from 10 and 11.
$\vdash \square \psi$, from 12.
$\vdash P$, from 13 and 10.

Reading it as a Turing machine

By interpreting $P$ as $halt(M)$ we can read the construction of $N$ as the definition of $\psi$, in fact that step requires the "diagonal lemma" pretty much the same of Kleene's recursion lemma but for logic formulas.

Our proof of the termination of $M$ is indeed the proof of Löb's theorem.