= Solution
Assume $S\vdash\neg X$ and $S\vdash BX\to X$. Combining these theorems gives $S\vdash\neg BX$. Because $X$ is refutable, $\neg BX$ is a legitimate <formal consistency statement> for $S$: the standard contradiction <first-order sentence> and $X$ are provably interderivable, and the <derivability conditions> transfer those implications to their provability statements.
Thus if $S$ were consistent, the <Gödel second incompleteness theorem> would contradict $S\vdash\neg BX$. Consequently the assumed reflection theorem forces $S$ to be inconsistent; <explosion> then gives $S\vdash X$. This establishes the instance of <Löb's theorem>
$$
\boxed{S\vdash BX\to X\quad\Longrightarrow\quad S\vdash X}
$$
for every $X$ refutable in $S$, using only the second incompleteness theorem.
Back to article page
