RUS  ENG
Полная версия
СЕМИНАРЫ

Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar"
25 сентября 2023 г. 18:30, г. Москва, МИАН (ул. Губкина, 8), ауд. 313 + Zoom


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

Н. Лукашов

Национальный исследовательский университет "Высшая школа экономики", г. Москва



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


© МИАН, 2024