A modal analysis of some principles of the provability logic of Heyting Arithmetic

Abstract

Besides the well-known principles K, K4 and L, the Leivant principle (AVВ)→ (AVB) and the Formalized Markov scheme  ¬¬ (A→ VBi) → (A→ VВi) are principles of the Provability Logic of (intuitionistic) Heyting Arithmetic. In this paper they are studied from a modal logical point of view. They are characterized, separate as well as in combination with the other principles, in terms of frame properties, and the finite model property is established. In order to make the paper self-contained intuitionistic modal logic is introduced and similar results for K4 and L, which were already known, are proved again.