On the unification problem for GLP
| Autor: | Beklemishev, Lev D. |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 19 pages |
| Databáze: | arXiv |
| Externí odkaz: |
|