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

Capa

Citar

Texto integral

Acesso aberto Acesso aberto
Acesso é fechado Acesso está concedido
Acesso é fechado Somente assinantes

Resumo

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.

Sobre autores

Lev Beklemishev

Steklov Mathematical Institute of Russian Academy of Sciences

Autor responsável pela correspondência
Email: lbekl@yandex.ru

Doctor of physico-mathematical sciences, no status

Moscow

Bibliografia

  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.

Arquivos suplementares

Arquivos suplementares
Ação
1. JATS XML
Baixar

Declaração de direitos autorais © Beklemishev L.D., 2025

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

 

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