= Hilbert-Bernays-Löb derivability conditions
{c}
{title2=$\Box(A\to B)\to(\Box A\to\Box B),\quad\Box A\to\Box\Box A$}
= Derivability conditions
{synonym}
For an <arithmetical provability predicate> write $\Box A=\operatorname{Pr}_T(\ulcorner A\urcorner)$. The conditions are: if $T\vdash A$ then $T\vdash\Box A$; $T\vdash\Box(A\to B)\to(\Box A\to\Box B)$; and $T\vdash\Box A\to\Box\Box A$. The first is an external rule, while the latter two are internal theorems. They formalize proof verification, closure under <modus ponens rule> and positive introspection. None licenses reflection from a proved sentence $\Box A$ to $A$.
Back to article page
