Provability logic and the completeness principle

The logic $\mathsf{iGLC}$ is the intuitionistic version of Löb's Logic plus the completeness principle $A\to \square A$. In this paper, we prove an arithmetical completeness theorems for $\mathsf{iGLC}$ for theories equipped with two provability predicates □ and △ that prove the schemes $A\to △A$ and $\square △S\to \square S$ for $S\in {\mathrm{\Sigma }}_1$. We provide two salient instances of the theorem. In the first, □ is fast provability and △ is ordinary provability and, in the second, □ is ordinary provability and △ is slow provability.Using the second instance, we reprove a theorem previously obtained by Mohammad Ardeshir and Mojtaba Mojtahedi 1] determining the ${\mathrm{\Sigma }}_1$-provability logic of Heyting Arithmetic.