Никита Лукашов//Алгебраическая унификация в модальных логиках

НИС "Современные проблемы математической логики" в ВШЭ.Дата и время: 11.04.2025 в 16:20

Докладчик: Никита Лукашов

Название: Алгебраическая унификация в модальных логиках

Аннотация:

Проблема символической унификации для логики L — это достаточно естественный вопрос, имеет ли данная формула \phi унификатор в логике L. Другими словами, существует ли такая подстановка \sigma для формулы \phi, что постановочный пример \sigma(\phi) является теоремой логики L. Несмотря на простоту формулировки, проблема унификации является довольно сложной, и ещё многое предстоит сделать в этой области.

В своём докладе я предоставлю алгебраический взгляд на проблему унификации в нормальных модальных логиках. Точнее мы посмотрим на проблему унификации в этих логиках с точки зрения алгебраической семантики. По ходу доклада, мы определим модальные алгебры для произвольных нормальных модальных логик и докажем их универсальные свойства. Затем мы подробно поговорим про проективные алгебры и их эквивалентные определения (в частности, покажем их связь с проективными формулами). После чего мы определим алгебраический тип унификации через эти проективные алгебры и докажем фундаментальные теорему, утверждающую, что два типа унификации — алгебраический и символический — для произвольных нормальных модальных логик совпадают.

В заключение, мы поговорим про точные формулы в нормальных модальных логиках, об условии, которое они задают для модальных алгебр, и получим новое алгебраическое доказательство известного факта, что проективные формулы всегда являются точными. Наконец, с помощью результатов С. Гильярди мы покажем, что в некоторых модальных логиках, таких как K4, S4, GL и др., верно обратное, т.е. точные и проективные формулы в этих логиках совпадают.