Provability logic and the completeness principle

Abstract The logic iGLC is the intuitionistic version of Lob's Logic plus the completeness principle A → □ A . In this paper, we prove an arithmetical completeness theorems for iGLC for theories equipped with two provability predicates □ and △ that prove the schemes A → △ A and □ △ S → □ S for S ∈ Σ 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 Σ 1 -provability logic of Heyting Arithmetic.