Geodesic
On the unification problem for $\mathrm{GLP}$
Izvestiya. Mathematics , Tome 89 (2025) no. 1, pp. 1-14.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: provability logic
Mots-clés : unification, admissible rule. 
@article{IM2_2025_89_1_a0,
     author = {L. D. Beklemishev},
     title = {On the unification problem for $\mathrm{GLP}$},
     journal = {Izvestiya. Mathematics },
     pages = {1--14},
     publisher = {mathdoc},
     volume = {89},
     number = {1},
     year = {2025},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IM2_2025_89_1_a0/}
}
TY  - JOUR
AU  - L. D. Beklemishev
TI  - On the unification problem for $\mathrm{GLP}$
JO  - Izvestiya. Mathematics 
PY  - 2025
SP  - 1
EP  - 14
VL  - 89
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IM2_2025_89_1_a0/
LA  - en
ID  - IM2_2025_89_1_a0
ER  - 
%0 Journal Article
%A L. D. Beklemishev
%T On the unification problem for $\mathrm{GLP}$
%J Izvestiya. Mathematics 
%D 2025
%P 1-14
%V 89
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IM2_2025_89_1_a0/
%G en
%F IM2_2025_89_1_a0
L. D. Beklemishev. On the unification problem for $\mathrm{GLP}$. Izvestiya. Mathematics , Tome 89 (2025) no. 1, pp. 1-14. http://geodesic.mathdoc.fr/item/IM2_2025_89_1_a0/

[1] J. P. Aguilera and F. Pakhomov, The logic of correct models, arXiv: 2402.15382

[2] S. N. Artemov and L. D. Beklemishev, “Provability logic”, Handbook of philosophical logic, Handb. Philos. Log., 13, 2nd ed., Springer, Dordrecht, 2005, 189–360 | DOI

[3] L. D. Beklemishev and J. J. Joosten, Problems collected at the Wormshop 2012 in Barcelona, 2012 https://homepage.mi-ras.ru/~bekl/Problems/worm_problems.pdf

[4] L. D. Beklemishev, “Provability algebras and proof-theoretic ordinals. I”, Ann. Pure Appl. Logic, 128:1-3 (2004), 103–123 | DOI | MR | Zbl

[5] L. D. Beklemishev, “Reflection principles and provability algebras in formal arithmetic”, Russian Math. Surveys, 60:2 (2005), 197–268 | DOI

[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 ; Logic Group Preprint Ser., 232, Utrecht Univ., 2004 https://dspace.library.uu.nl/handle/1874/26864 | Zbl

[7] L. D. Beklemishev, “Kripke semantics for provability logic GLP”, Ann. Pure Appl. Logic, 161:6 (2010), 756–774 | DOI | MR | Zbl

[8] L. D. Beklemishev, “A simplified proof of arithmetical completeness theorem for provability logic $\mathbf{GLP}$”, Proc. Steklov Inst. Math., 274 (2011), 25–33 | DOI

[9] L. D. Beklemishev, “On the reduction property for GLP-algebras”, Dokl. Math., 95:1 (2017), 50–54 | DOI

[10] L. D. Beklemishev, J. J. Joosten, and M. Vervoort, “A finitary treatment of the closed fragment of Japaridze's provability logic”, J. Logic Comput., 15:4 (2005), 447–463 | DOI | MR | Zbl

[11] N. Bezhanishvili, D. Gabelaia, S. Ghilardi, and M. Jibladze, “Admissible bases via stable canonical rules”, Studia Logica, 104:2 (2016), 317–341 | DOI | MR | Zbl

[12] S. Feferman, “Arithmetization of metamathematics in a general setting”, Fund. Math., 49 (1960), 35–92 | DOI | MR | Zbl

[13] S. Ghilardi, “Unification in intuitionistic logic”, J. Symbolic Logic, 64:2 (1999), 859–880 | DOI | MR | Zbl

[14] S. Ghilardi, “Best solving modal equations”, Ann. Pure Appl. Logic, 102:3 (2000), 183–198 | DOI | MR | Zbl

[15] T. Icard, “A topological study of the closed fragment of GLP”, J. Logic Comput., 21:4 (2011), 683–696 | DOI | MR | Zbl

[16] R. Iemhoff, “On the admissible rules of intuitionistic propositional logic”, J. Symb. Log., 66:1 (2001), 281–294 | DOI | MR | Zbl

[17] R. Iemhoff and G. Metcalfe, “Proof theory for admissible rules”, Ann. Pure Appl. Logic, 159:1-2 (2009), 171–186 | DOI | MR | Zbl

[18] K. N. Ignatiev, “On strong provability predicates and the associated modal logics”, J. Symb. Log., 58:1 (1993), 249–290 | DOI | MR | Zbl

[19] G. K. Japaridze, Modal logic tools of investigation of provability, Candidate (PhD) dissertation, Moscow State Univ., Moscow, 1986 (Russian)

[20] E. Jeřábek, “Admissible rules of modal logics”, J. Logic Comput., 15:4 (2005), 411–431 | DOI | MR | Zbl

[21] E. Jeřábek, “Blending margins: The modal logic K has nullary unification type”, J. Logic Comput., 25:5 (2015), 1231–1240 | DOI | MR | Zbl

[22] E. Kolmakov and L. Beklemishev, “Axiomatization of provable $n$-provability”, J. Logic Comput., 84:2 (2019), 849–869 | DOI | MR | Zbl

[23] N. Lukashov, Unification problem for the provability logic GLP, Bachelor Thesis, Nat. Res. Univ. Higher School Econ. Faculty Math., Moscow, 2023 (Russian)

[24] F. N. Pakhomov, “Linear $\mathrm{GLP}$-algebras and their elementary theories”, Izv. Math., 80:6 (2016), 1159–1199 | DOI

[25] V. V. Rybakov, “A criterion for admissibility of rules in the modal system $\mathrm{S4}$ and intuitionistic logic”, Algebra and Logic, 23:5 (1984), 369–384 | DOI

[26] V. V. Rybakov, “Admissibility of rules of inference in the modal system $G$”, Trudy Inst. Mat. Sib. Otd. AN SSSR, 12 (1989), 120–138 (Russian) | MR | Zbl

[27] V. V. Rybakov, Admissibility of logical inference rules, Stud. Logic Found. Math., 136, North-Holland Publishing Co., Amsterdam, 1997 | MR | Zbl

[28] D. S. Shamkanov, “Interpolation properties for provability logics $\mathbf{GL}$ and $\mathbf{GLP}$”, Proc. Steklov Inst. Math., 274 (2011), 303–316 | DOI

[29] F. Wolter and M. Zakharyaschev, “Undecidability of the unification and admissibility problems for modal and description logics”, ACM Trans. Comput. Log., 9:4 (2008), 25 | DOI | MR | Zbl