О проблеме унификации для полимодальной логики доказуемости

Проблема унификации для данной модальной логики тесно связана с проблемой характеризации ее допустимых правил вывода. Хорошо известно, что логика GL имеет конечный унификационный тип (С. Гилярди), проблема допустимости правил вывода в GL алгоритмически разрешима (В.В. Рыбаков) и ее допустимые правила вывода имеют естественную аксиоматизацию (Э. Ержабек). Для полимодальной логики доказуемости GLP, в том числе и для языка всего с двумя модальностями, эти вопросы пока остаются открытыми.
Мы докажем, что финитно аппроксимируемый фрагмент J полимодальной логики доказуемости GLP (в языке с конечным числом модальностей) имеет конечный унификационный тип, то есть множество унификаторов любой формулы порождается конечным числом максимальных. В то же время унификационный тип самой логики GLP уже для языка с двумя модальностями - нулевой, то есть существует унифицируемая формула, множество унификаторов которой не имеет максимального.
Совместная работа с Л.Д. Беклемишевым.