= Solution
Put $T=S\cup\{\neg X\}$ and assume $S\vdash P_S(\ulcorner X\urcorner)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(\ulcorner X\urcorner)$.
Classical logic proves $(\neg X\to X)\to X$. By the <derivability conditions>,
$$
S\vdash P_S(\ulcorner\neg X\to X\urcorner)\to P_S(\ulcorner X\urcorner).
$$
Compose this with the supplied formalized deduction implication from $P_T(\ulcorner X\urcorner)$ to its left-hand side. Then $T$ proves
$$
P_T(\ulcorner X\urcorner)\to P_S(\ulcorner X\urcorner),
$$
and therefore
$$
T\vdash\neg P_T(\ulcorner X\urcorner).
$$
The other supplied assumption says this is impossible if $T$ is <first-order consistent>. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S\vdash\neg\neg X$, hence
$$
\boxed{S\vdash X.}
$$
This establishes Löb's <inference rule> using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.
Back to article page
