Unification in subsystem J₂ of provability logic GLB

We generalize methods, developed by S. Ghilardi, and apply them to a subsystem J₂ of bimodal provability logic GLB. We describe projective formulas in J₂ in terms of Kripke semantics and prove that logic J₂ has finitary unification type. As an application, we show that admissibility problem for J₂ is decidable.