Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 2 / d

Put $T=S+\{X\}$ and choose its Gödel sentence $Z$, so $T⊢Z\leftrightarrow \neg B_{T}Z$. The assumed reflection scheme gives the particular theoremThe given extension-provability implication is $S⊢B_{T}Z\to B_S(X\to Z)$. The fixed-point equivalence gives $T⊢\neg Z\to B_{T}Z$, so these implications compose toThe supplied propositional tautology $((\neg Z\to (X\to Z))\to (X\to Z))$ gives $T⊢X\to Z$, and $T⊢X$ then yields $T⊢Z$. The first of the derivability conditions for $T$ gives $T⊢B_{T}Z$, while its Gödel equivalence gives $T⊢\neg B_{T}Z$. Hence $T$ is inconsistent. By the deduction theorem for propositional logic,This proof uses diagonalization and proof transfer for the extension, and invokes neither Löb's theorem nor the second incompleteness theorem.