Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2008 / A / 3 / b

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe 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⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.