Provability Logic and the Completeness Principle

Abstract

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 $\square$ and $△$ that prove the schemes $A\to △A$ and $\square △S\to \square S$ for $S\in {\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 ${\Sigma }_1$-provability logic of Heyting Arithmetic.