On provability logic of HA

In this talk we are going to present a sketch of the proof for axiomatization and decidability of provability logic of HA. At the beginning we explain how admissibility and unification for the intuitionistic logic can be relativised to NNIL, the class of fomulas with No Nested Implications in the Left. Using this, we axiomatize several preservativity and admissibility relations for intuitionistic modal logics. Then we introduce the provability semantics in the form of a specific Kripke-style semantics. The truth of $\Box A$ at a paticular node in the sense of this semantics uses the derivability in a specific modal logic associated with the accessible nodes. Finally, we use such semantics to reduce the arithmetical completeness of the provability logic of HA to the one for its $\Sigma_1$ version.
P.S.: This is a first presentation for two manuscripts which are not refereed yet. You may find them on my home page (items 11 and 12): http://pub.mmojtahedi.ir/.