Никита Лукашов//Проективность и свойство расширения для логики GL (Часть 2)

НИС "Современные проблемы математической логики" в ВШЭ. Дата и время: 24.10.2025 в 16:20 Название: Проективность и свойство расширения для логики GL, Часть II Докладчик: Никита Лукашов Аннотация: В первой части доклада мы подробно рассмотрели проблему унификации для логик, обсудили определение типа унификации для них, а также привели полное доказательство того, что классическая пропозициональная логика CL обладает унитарным типом унификации. Для установления последнего результата мы использовали так называемые проективные формулы, определение которых мы привели для произвольных логик и доказали их основные свойства. Во второй части доклада мы продолжим доказательство семантической характеризации С. Гилярди (2000 г.) проективных формул для модальных логик на примере конкретной модальной логике доказуемости GL. Я коротко напомню про семантический подход к проблеме унификации из первой части, а затем перейду к рассказу доказательства того, что формула A является проективной в логике GL тогда и только тогда, когда класс MOD(A) конечных GL-моделей Крипке с корнем формулы A обладает некоторым определённым свойством расширения. Если останется время, то я также расскажу, как из полученной семантической характеризации проективных формул доказать конечный тип унификации логики GL (соответственно, рассуждение из второй части статьи ниже). Доклад основан на статье: Ghilardi S. Best solving modal equations //Annals of Pure and Applied Logic. – 2000. – Т. 102. – №. 3. – С. 183-198.