论 GLP 的合一问题
On the unification problem for GLP
AI总结：
本文研究多模态可证性逻辑 GLP 的合一类型，证明其为零元，给出公式 [1]p 的无穷完备合一元集，并说明可合一性判定可解。
摘要：
我们证明，在至少包含两个模态词和一个变元的语言中，多模态可证性逻辑 GLP 具有零元合一类型。更具体地说，我们证明公式 [1]p 不存在极大合一元，并为其构造一个无穷的完备合一元集合。此外，我们讨论判定给定公式在 GLP 中是否可合一的算法问题，并指出该问题有肯定解。最后，我们陈述 GLP 的合一问题与可容许性问题的算术对应形式，并提出若干开放问题。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
