Related to: Löb's Theorem for implicit reasoning in natural language: Löbian party invitations

tl;dr: Löb's Theorem is much easier to grok if you separate the parts of the proof that use the assumption from the parts that don't. The parts that don't use $□ p \to p$ can be extracted as a stand-alone result, which I hereby dub "Löb's Lemma".

Here's how it works.

Key properties of $⊢$ and $□$

Here is some standard notation. In short, $⊢$ is our symbol for talking about what PA can prove, and $□$ is shorthand for PA's symbols for talking about what (a copy of) PA can prove.

" $⊢$ 1+1=2" means "Peano Arithmetic (PA) can prove that 1+1=2". No parentheses are needed; the " $⊢$ " applies to the whole line that follows it. Also, $⊢$ does not stand for an expression in PA; it's a symbol we use to talk about what PA can prove.
" $□ (1+1=2)$ " basically means the same thing. More precisely, it stands for a numerical expression within PA that can be translated as saying " $⊢$ 1+1=2". This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself.
" $□ X$ " is short for " $□ (X)$ " in cases where " $X$ " is just a single character of text.
" $X ⊢ Y$ " means "PA, along with X as an additional axiom/assumption, can prove Y". In this post we don't have any analogous notation for $□$ .

The proofs here will use the following standard properties of $⊢$ and $□$ (source: Wikipedia), which respectively stand for provability and provability encoded within arithmetic.

(necessitation) From $⊢ A$ , conclude $⊢ □ A$ . Informally, this says that if A can be proven, then it can be proven that it can be proven (by just writing out and checking the proof within arithmetic). Note that from $X ⊢ A$ we cannot conclude $X ⊢ □ A$ , because $□$ still means "PA can prove", and not "PA+X can prove".

(internal necessitation) $⊢ □ A \to □ □ A$ . If A is provable, then it is provable that it is provable (basically the same as the previous point).
(box distributivity) $⊢ □ (A \to B) \to (□ A \to □ B)$ . This rule allows one to apply modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.
(deduction theorem) From $A ⊢ B$ , conclude $⊢ A \to B$ : if assuming $A$ is enough to prove $B$ , then it's possible to prove under no assumptions that $A \to B$ .

Point 4 is helpful and pretty intuitive, but for whatever reason isn't used in the main Wikipedia article on Löb's Theorem.

Löb's Lemma

Claim: Assume $Ψ$ and $p$ are any statements satisfying $⊢ Ψ \leftrightarrow □ Ψ \to p$ . Then $⊢ □ Ψ \leftrightarrow □ p$ .

Intuition: By assumption, the sentence $Ψ$ is equivalent to saying "If this sentence is provable, then $p$ ". Intuitively, $Ψ$ has very little content, except for the $p$ part at the end, so it makes sense that $□ Ψ$ boils down to nothing more than $□ p$ in terms of logical equivalence.

Reminder: this does not use the assumption $□ p \to p$ from Löb's Theorem at all.

Proof:

Let's do the forward implication first:

$□ Ψ ⊢ □ □ Ψ$ by internal necessitation ( $□ Ψ \to □ □ Ψ$ ).
$□ Ψ ⊢ □ (□ Ψ \to p)$ using box distributivity on the assumption,
with $A = Ψ$ and $B = □ Ψ \to p$ .
$□ Ψ ⊢ □ p$ from 1 and 2 by box distributivity.
$⊢ □ Ψ \to □ p$ from 3 by the deduction theorem.

Now for the backwards implication, which isn't needed for Löb's Theorem, but is handy anyway:

$⊢ p \to (□ Ψ \to p)$ is a tautology.
$⊢ □ p \to □ (□ Ψ \to p)$ by box distributivity on 1.
$⊢ □ Ψ \leftrightarrow □ (□ Ψ \to p)$ by box distributivity on the assumption.
$⊢ □ p \to □ Ψ$ by 2 and 3.

I like this result because both directions of the proof are fairly short, it doesn't use the assumption $□ p \to p$ at all, and the conclusion itself is also fairly intuitive. The statement $Ψ$ just turns out to have no content except for $p$ itself, from the perspective of writing proofs.

Löb's Theorem, now in just 6 lines

If you can remember Löb's Lemma, you can write a very straightforward proof of Löb's Theorem in just 6 lines:

Claim: If $p$ is any sentence such that $⊢ □ p \to p$ , then $⊢ p$

Proof:

Let $Ψ$ be any sentence satisfying $⊢ Ψ \leftrightarrow (□ Ψ \to p)$ , which exists by the existence of modal fixed points (or by the Diagonal Lemma).

$⊢ □ Ψ \to □ p$ by Löb's Lemma.
$⊢ □ p \to p$ by assumption.
$⊢ □ Ψ \to p$ by 1 and 2 combined.
$⊢ Ψ$ by 3 and the defining property of $Ψ$
$⊢ □ Ψ$ by necessitation.
$⊢ p$ by 3 and 5.

«mic drop»