= Full local reflection in a one-sentence extension is inconsistent
Assume the <Hilbert-Bernays-Löb derivability conditions> and the <diagonal lemma>. If $T+X$ proves $\operatorname{Pr}_T(\ulcorner Y\urcorner)\to Y$ for every sentence $Y$, then $T\vdash\neg X$. Take the single instance $Y=\neg X$ and discharge the assumption: $T\vdash X\to(\Box\neg X\to\neg X)$. This propositionally implies $T\vdash\Box\neg X\to\neg X$, and <Löb's theorem> gives $T\vdash\neg X$. A diagonal proof is also possible using the <Gödel sentence> of the extension and formalized proof transfer, without appealing to Löb's theorem.
Back to article page
