= Solution
Use just the assumed local reflection instance with $Y=\neg X$:
$$
S+\{X\}\vdash B_S(\neg X)\to\neg X.
$$
By the <deduction theorem for propositional logic>, $S\vdash X\to(B_S(\neg X)\to\neg X)$. <Classical propositional logic> makes this imply the unconditional reflection statement $S\vdash B_S(\neg X)\to\neg X$: if $X$ is false the consequent is already true, and if $X$ is true the displayed implication supplies it. <Löb's theorem> applied to $\neg X$ now gives
$$
\boxed{S\vdash\neg X.}
$$
Thus <full local reflection in a one-sentence extension is inconsistent>; in this argument even the single instance concerning $\neg X$ suffices.
Back to article page
