= Löb's theorem
{c}
{title2=$T\vdash(\Box A\to A)\Longrightarrow T\vdash A$}
{wiki}
Assume the <Hilbert-Bernays-Löb derivability conditions> and the <diagonal lemma>. Choose $D$ with $T\vdash D\leftrightarrow(\Box D\to A)$. Necessitating the forward implication and using distribution and positive introspection gives $T\vdash\Box D\to\Box A$. If $T\vdash\Box A\to A$, then $T\vdash\Box D\to A$, so the reverse fixed-point implication gives $T\vdash D$. Necessitation gives $T\vdash\Box D$, and the preceding implications give $T\vdash A$. No consistency assumption is needed for this implication between provability assertions.
Back to article page
