Solution (source code)

= Solution

Suppose $S+A$ proves every specified <full local reflection in a one-sentence extension is inconsistent>[reflection] instance. Use only the instance with $X=\neg A$. The <deduction theorem for first-order logic>[deduction theorem] gives
$$
S\vdash A\to(\Box\neg A\to\neg A).
$$
<classical propositional logic>[Classical propositional reasoning] turns this into $S\vdash\Box\neg A\to\neg A$: if $\neg A$ already holds the implication is true, while otherwise $A$ holds and the displayed theorem supplies it. <Löb's theorem> now yields $S\vdash\neg A$, making $S+A$ <consistent first-order theory>[inconsistent]. Therefore \b[no sentence <consistent first-order theory>[consistent] with $S$ can supply all the local <full local reflection in a one-sentence extension is inconsistent>[reflection] instances in a one-sentence extension]. The proof uses just one well-chosen instance, and never applies <necessitation rule>[necessitation] to a derivation with the extra assumption still open.