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 wellknown 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.