We axiomatize the provability logic of $\HA$ and prove its decidability. Furthermore, we axiomatize the preservativity and relative admissibility relations for several modal logics extending iK4. A principal technical tool is the introduction of a new type of semantics, termed \emph{provability models}, for modal logics extending iGL. This semantics combines elements of standard Kripke semantics with provability in propositional modal logics.