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