Proof of Löb's theorem

The intuition behind the proof of Löb's theorem invokes the formalization of the following argument:

Let $S$ stand for the sentence "If $S$ is provable, then I am Santa Claus".

As it is standard, when trying to prove a If...then theorem we can start by supposing the antecedent and checking that the consequent follows. But if $S$ is provable, then we can chain its proof to an application of modus ponens of $S$ to itself in order to get a proof of the consequent "I am Santa Claus". If we suppose that showing the existence of a proof of a sentence implies that the sentence is true, then "I am Santa Claus" is true.

Thus we have supposed that $S$ is provably true then it follows that "I am Santa Claus", which is a proof of what $S$ states! Therefore, $S$ is provably true, and we can apply the same reasoning again (this time without supposing a counterfactual) to get that it is true that "I am Santa Claus".

Holy Gödel! Have we broken logic? If this argument worked, then we could prove any nonsensical thing we wanted. So where does it fail?

One suspicious point is our implicit assumption that $S$ can be constructed in the first place as a first order sentence. But we know that there exists a provability predicate encoding the meaning we need, and then we can apply the diagonal lemma to the formula $Prv\left(x\right)⟹$ "I am Santa Claus" to get our desired $S$.

(We will ignore the fact that expressing "I am Santa Claus" in the language of first order logic is rather difficult, since we could easily replace it with something simple like $0=1$.)

It turns out that the culprit of this paradox is the apparently innocent supposition that when "I am Santa Claus" is provable, then it is true.

How can this be false?, you may ask. Well, the standard provability predicate $Prv$ is something of the form $\exists yProof(x,y)$, where $Proof(x,y)$ is true iff $y$ encodes a valid proof of $x$. But $y$ might be a nonstandard number encoding a nonstandard proof of infinitely many steps. If the only proofs of $x$ are nonstandard then certainly you will never be able to prove $x$ from the axioms of the system using standard methods.

We can restate this result as Löb's theorem: If $Prv\left(A\right)⟹A$ is provable, then $A$ is provable.

Now we go for the formal proof.

Let $T$ be an axiomatizable extension of minimal arithmetic, and $P$ a one-place predicate satisfying the Bernais-Hilbert derivability conditions, which are:

1. If $T⊢A$, then $T⊢P\left(A\right)$.
2. $T⊢P(A⟹B)⟹\left(P\right(A)⟹P(B\left)\right)$
3. $T⊢P\left(A\right)⟹P\left(P\right(A\left)\right)$.

For example, $PA$ and the standard provability predicate satisfy those conditions.

Let us suppose that $A$ is such that $T⊢P\left(A\right)⟹A$.

As $T$ extends minimal arithmetic, the diagonal lemma is applicable, and thus there exists $S$ such that $T⊢S⟺\left(P\right(S)⟹A)$.

By condition 1, $T⊢P(S⟹(P\left(S\right)⟹A\left)\right)$.

By condition 2, $T⊢P\left(S\right)⟹P\left(P\right(S)⟹A)$.

Also by condition 2, $T⊢P\left(P\right(S)⟹A)⟹\left(P\right(P\left(S\right))⟹P(A\left)\right)$.

Combining these, $T⊢P\left(S\right)⟹\left(P\right(P\left(S\right))⟹P(A\left)\right)$.

By condition 3, $T⊢P\left(S\right)⟹P\left(P\right(S\left)\right)$ and thus $T⊢P\left(S\right)⟹P\left(A\right)$.

By our initial assumption, this means that $T⊢P\left(S\right)⟹A$.

But by the construction of $S$, then $T⊢S$!

By condition 1 again, then $T⊢P\left(S\right)$, and since we already had shown that $T⊢P\left(S\right)⟹A$, we have that $T⊢A$, which completes the proof.

We remark that $P$ can be any predicate satisfying the conditions, such as the verum predicate $x=x$.