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

Assume $S⊢\neg X$ and $S⊢BX\to X$. Combining these theorems gives $S⊢\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⊢\neg BX$. Consequently the assumed reflection theorem forces $S$ to be inconsistent; explosion then gives $S⊢X$. This establishes the instance of Löb's theoremfor every $X$ refutable in $S$, using only the second incompleteness theorem.