= Solution
<Löb's theorem> states that, for a <first-order theory> with the stated provability and diagonalization properties,
$$
\boxed{S\vdash(BA\to A)\quad\Longrightarrow\quad S\vdash A,}
$$
where $BA=P_S(\ulcorner A\urcorner)$. It does not require an extra consistency assumption.
By the <diagonal lemma>, choose $D$ with $S\vdash D\leftrightarrow(BD\to A)$. <necessitation rule> and distribution applied to $D\to(BD\to A)$ give
$$
S\vdash BD\to B(BD\to A),\qquad S\vdash BD\to(B(BD)\to BA).
$$
Using <positive introspection> $BD\to B(BD)$ gives the unconditional theorem $S\vdash BD\to BA$. If $S\vdash BA\to A$, it follows that $S\vdash BD\to A$, and the reverse fixed-point implication gives $S\vdash D$. Necessitating gives $S\vdash BD$, hence $S\vdash BA$ and finally $S\vdash A$.
The same derivation also gives the <Internal form of Löb's theorem>, needed for modal soundness. Put $H=(BA\to A)$. From the unconditional $BD\to BA$, propositional reasoning and the fixed point give $S\vdash H\to D$. <necessitation rule> and distribution imply $S\vdash BH\to BD$, and hence
$$
\boxed{S\vdash B(BA\to A)\to BA.}
$$
This internal statement was derived without necessitating a temporary assumption.
Back to article page
