2024/04/07 by Beklemishev, Lev D.
#03B45 #03F45 #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.2404.04893
We show that the polymodal provability logic GLP, in a language with at least two modalities and one variable, has nullary unification type. More specifically, we show that the formula [1]p does not have maximal unifiers, and exhibit an infinite complete set of unifiers 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.