Unification in subsystems of polymodal provability logic GLP

Abstract We show that subsystems $\textrm{J}_{t}$ of the polymodal provability logic $\textrm{GLP}$ in the language with $t$ modalities have a finitary unification type. Furthermore, we prove that the unification problems for $\textrm{J}_{t}$ and $\textrm{J}$ and the problem of recognizing admissible rules for $\textrm{J}_{t}$ are decidable. Near the end we prove that the unification type of the entire logic $\textrm{J}$ with infinitely many modalities is nullary.