= Solution
Assume $S\vdash B_SX\to X$ and put $T=S+\{\neg X\}$. Then $T\vdash\neg B_SX$. The given extension-provability implication, with $Y=\bot$, gives
$$
S\vdash B_T\bot\to B_S(\neg X\to\bot).
$$
The provable classical implication $(\neg X\to\bot)\to X$, together with distribution, gives $S\vdash B_S(\neg X\to\bot)\to B_SX$. Hence
$$
T\vdash B_T\bot\to B_SX,\qquad T\vdash\neg B_T\bot=\operatorname{Con}(T).
$$
If $T$ were consistent, this would violate its <Gödel second incompleteness theorem>. Thus $T$ is inconsistent. The <deduction theorem for propositional logic> and double-negation elimination give $S\vdash\neg\neg X$, hence $S\vdash X$. Therefore \b[the second incompleteness theorem for $S+\{\neg X\}$ yields <Löb's theorem> for arbitrary $X$].
Back to article page
