= Internal form of Löb's theorem
{c}
{title2=$T\vdash\Box(\Box A\to A)\to\Box A$}
In the <Löb's theorem> proof, $T\vdash\Box D\to\Box A$ is obtained before any reflection assumption. Put $H=(\Box A\to A)$. Propositional reasoning and the diagonal equation give $T\vdash H\to D$. Necessitation and distribution yield $T\vdash\Box H\to\Box D$, hence the displayed implication. This is the arithmetic interpretation of the Löb axiom in <Gödel-Löb logic>, and avoids necessitating a temporary assumption.
Back to article page
