A Modal Analysis of Some Principles of the Provability Logic of Heyting Arithmetic Rosalie Iemhoff Abstract: A Modal Analysis of some Principles of the Provability Logic of Heyting Arithmetic Rosalie Iemhoff In this paper four principles and one scheme of the Provability Logic of (intuitionistic) Heyting Arithmetic HA are studied from a modal-logical point of view. These are, besides the well­known principles K, K4 and L of the Provability Logic of Peano Arithmetic, the principle [](A v B) -> [](A v [] B) and the scheme []--([]A -> V []B_i) -> []([]A -> V []B_i). Intuitionistic modal logic is introduced. And for all principles and for the scheme considered (seperately and together) frame completeness is proved, and the finite model property is established.