Provability Logic and the Completeness Principle

In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\mathrm{\square }$ and $\mathrm{△}$ that prove the schemes $A\to \mathrm{△}A$ and $\mathrm{\square }\mathrm{△}S\to \mathrm{\square }S$ for $S\in {\mathrm{\Sigma }}_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the ${\mathrm{\Sigma }}_1$-provability logic of Heyting Arithmetic.