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.

Согласие на обработку персональных данных с помощью сервиса «Яндекс.Метрика»

1. Я (далее – «Пользователь» или «Субъект персональных данных»), осуществляя использование сайта https://journals.rcsi.science/ (далее – «Сайт»), подтверждая свою полную дееспособность даю согласие на обработку персональных данных с использованием средств автоматизации Оператору - федеральному государственному бюджетному учреждению «Российский центр научной информации» (РЦНИ), далее – «Оператор», расположенному по адресу: 119991, г. Москва, Ленинский просп., д.32А, со следующими условиями.

2. Категории обрабатываемых данных: файлы «cookies» (куки-файлы). Файлы «cookie» – это небольшой текстовый файл, который веб-сервер может хранить в браузере Пользователя. Данные файлы веб-сервер загружает на устройство Пользователя при посещении им Сайта. При каждом следующем посещении Пользователем Сайта «cookie» файлы отправляются на Сайт Оператора. Данные файлы позволяют Сайту распознавать устройство Пользователя. Содержимое такого файла может как относиться, так и не относиться к персональным данным, в зависимости от того, содержит ли такой файл персональные данные или содержит обезличенные технические данные.

3. Цель обработки персональных данных: анализ пользовательской активности с помощью сервиса «Яндекс.Метрика».

4. Категории субъектов персональных данных: все Пользователи Сайта, которые дали согласие на обработку файлов «cookie».

5. Способы обработки: сбор, запись, систематизация, накопление, хранение, уточнение (обновление, изменение), извлечение, использование, передача (доступ, предоставление), блокирование, удаление, уничтожение персональных данных.

6. Срок обработки и хранения: до получения от Субъекта персональных данных требования о прекращении обработки/отзыва согласия.

7. Способ отзыва: заявление об отзыве в письменном виде путём его направления на адрес электронной почты Оператора: info@rcsi.science или путем письменного обращения по юридическому адресу: 119991, г. Москва, Ленинский просп., д.32А

8. Субъект персональных данных вправе запретить своему оборудованию прием этих данных или ограничить прием этих данных. При отказе от получения таких данных или при ограничении приема данных некоторые функции Сайта могут работать некорректно. Субъект персональных данных обязуется сам настроить свое оборудование таким способом, чтобы оно обеспечивало адекватный его желаниям режим работы и уровень защиты данных файлов «cookie», Оператор не предоставляет технологических и правовых консультаций на темы подобного характера.

9. Порядок уничтожения персональных данных при достижении цели их обработки или при наступлении иных законных оснований определяется Оператором в соответствии с законодательством Российской Федерации.

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