О проблеме унификации для логики GLP

We show that the polymodal provability logic GLP, in a language with at least two modalities and one variable, has nullary uni cation type. More speci cally, we show that the formula [1]p does not have maximal unifiers, and exhibit an infinite complete set of uni ers for it. Further, we discuss the algorithmic problem of whether a given formula is unifiable in GLP and remark that this problem has a positive solution. Finally, we state the arithmetical analogues of the unification and admissibility problems for GLP and formulate a number of open questions.