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/