On the unification problem for $\mathrm{GLP}$

Cover Page

Cite item

Full Text

Open Access Open Access
Restricted Access Access granted
Restricted Access Subscription Access

Abstract

We show that the polymodal provability logic $\mathrm{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 $\mathrm{GLP}$ and remark that this problem has a positive solution. Finally, we state the arithmetical analogues of the unification and admissibility problems for $\mathrm{GLP}$ and formulate a number of open questions.

About the authors

Lev Dmitrievich Beklemishev

Steklov Mathematical Institute of Russian Academy of Sciences

Author for correspondence.
Email: lbekl@yandex.ru

Doctor of physico-mathematical sciences, no status

Moscow

References

  1. J. P. Aguilera, F. Pakhomov, The logic of correct models
  2. S. N. Artemov, L. D. Beklemishev, “Provability logic”, Handbook of philosophical logic, Handb. Philos. Log., 13, 2nd ed., Springer, Dordrecht, 2005, 189–360
  3. L. D. Beklemishev, J. J. Joosten, Problems collected at the Wormshop 2012 in Barcelona, 2012
  4. L. D. Beklemishev, “Provability algebras and proof-theoretic ordinals. I”, Ann. Pure Appl. Logic, 128:1-3 (2004), 103–123
  5. Л. Д. Беклемишев, “Схемы рефлексии и алгебры доказуемости в формальной арифметике”, УМН, 60:2(362) (2005), 3–78
  6. L. D. Beklemishev, “Veblen hierarchy in the context of provability algebras”, Logic, methodology and philosophy of science (Oviedo, Spain, 2003), King's College Publ., London, 2005, 65–78
  7. L. D. Beklemishev, “Kripke semantics for provability logic GLP”, Ann. Pure Appl. Logic, 161:6 (2010), 756–774
  8. Л. Д. Беклемишев, “Упрощенное доказательство теоремы об арифметической полноте для логики доказуемости $mathbf{GLP}$”, Алгоритмические вопросы алгебры и логики, Сборник статей. К 80-летию со дня рождения академика Сергея Ивановича Адяна, Тр. МИАН, 274, МАИК «Наука/Интерпериодика», М., 2011, 32–40
  9. Л. Д. Беклемишев, “О свойстве редукции для $GLP$-алгебр”, Докл. РАН, 472:4 (2017), 378–382
  10. L. D. Beklemishev, J. J. Joosten, M. Vervoort, “A finitary treatment of the closed fragment of Japaridze's provability logic”, J. Logic Comput., 15:4 (2005), 447–463
  11. N. Bezhanishvili, D. Gabelaia, S. Ghilardi, M. Jibladze, “Admissible bases via stable canonical rules”, Studia Logica, 104:2 (2016), 317–341
  12. S. Feferman, “Arithmetization of metamathematics in a general setting”, Fund. Math., 49 (1960), 35–92
  13. S. Ghilardi, “Unification in intuitionistic logic”, J. Symbolic Logic, 64:2 (1999), 859–880
  14. S. Ghilardi, “Best solving modal equations”, Ann. Pure Appl. Logic, 102:3 (2000), 183–198
  15. T. Icard, “A topological study of the closed fragment of GLP”, J. Logic Comput., 21:4 (2011), 683–696
  16. R. Iemhoff, “On the admissible rules of intuitionistic propositional logic”, J. Symb. Log., 66:1 (2001), 281–294
  17. R. Iemhoff, G. Metcalfe, “Proof theory for admissible rules”, Ann. Pure Appl. Logic, 159:1-2 (2009), 171–186
  18. K. N. Ignatiev, “On strong provability predicates and the associated modal logics”, J. Symb. Log., 58:1 (1993), 249–290
  19. Г. К. Джапаридзе, Модально-логические средства исследования доказуемости, Дисс. … канд. филос. наук, МГУ, М., 1986, 177 с.
  20. E. Jeřabek, “Admissible rules of modal logics”, J. Logic Comput., 15:4 (2005), 411–431
  21. E. Jeřabek, “Blending margins: The modal logic K has nullary unification type”, J. Logic Comput., 25:5 (2015), 1231–1240
  22. E. Kolmakov, L. Beklemishev, “Axiomatization of provable $n$-provability”, J. Logic Comput., 84:2 (2019), 849–869
  23. Н. Лукашов, Проблема унификации в бимодальной логике доказуемости GLB, ВКР, НИУ ВШЭ, Ф-т матем., М., 2023
  24. Ф. Н. Пахомов, “Линейные $mathrm{GLP}$-алгебры и их элементарные теории”, Изв. РАН. Сер. матем., 80:6 (2016), 173–216
  25. В. В. Рыбаков, “Критерий допустимости правил в модальной системе $mathrm{S}4$ и интуиционистской логике”, Алгебра и логика, 23:5 (1984), 546–572
  26. В. В. Рыбаков, “О допустимости правил вывода в модальной системе $G$”, Тр. Ин-та математики, 12 (1989), 120–138
  27. V. V. Rybakov, Admissibility of logical inference rules, Stud. Logic Found. Math., 136, North-Holland Publishing Co., Amsterdam, 1997, ii+617 pp.
  28. Д. С. Шамканов, “Интерполяционные свойства логик доказуемости $mathbf{GL}$ и $mathbf{GLP}$”, Алгоритмические вопросы алгебры и логики, Сборник статей. К 80-летию со дня рождения академика Сергея Ивановича Адяна, Труды МИАН, 274, МАИК «Наука/Интерпериодика», М., 2011, 329–342
  29. F. Wolter, M. Zakharyaschev, “Undecidability of the unification and admissibility problems for modal and description logics”, ACM Trans. Comput. Log., 9:4 (2008), 25, 20 pp.

Supplementary files

Supplementary Files
Action
1. JATS XML
Download

Copyright (c) 2025 Beklemishev L.D.

Согласие на обработку персональных данных

 

Используя сайт https://journals.rcsi.science, я (далее – «Пользователь» или «Субъект персональных данных») даю согласие на обработку персональных данных на этом сайте (текст Согласия) и на обработку персональных данных с помощью сервиса «Яндекс.Метрика» (текст Согласия).