Necessitation rule
= Necessitation rule
{title2=$\vdash A\Longrightarrow\vdash\Box A$}
The <necessitation rule> permits boxing a theorem in a modal proof system. It does not permit boxing an arbitrary temporary assumption. Under an arithmetic interpretation, it uses the external first of the <derivability conditions>: an actual proof of $A$ supplies a proof that $A$ has a proof. This distinction matters when proving the <Internal form of Löb's theorem>.