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.