 For such theories, arithmetical soundness and completeness of GL hold, provided that \(\Box\) translates to \(\Prov_T\), a natural provability predicate with respect to a sufficiently simple axiomatization of \(T\). Thus for modal sentences \(A\):