Модальная логика
(годовой спецкурс, 2018—2019)
с.н.с. Е.Е.Золин

Краткое содержание лекций (осенний семестр 2018 года):
  1. 2018.09.14: (Вводная лекция) Краткий обзор: различные семантики модальной логики (понимания связки «необходимость»): семантика возможных миров (Крипке), алгебраическая, топологическая, доказуемостная семантика.
    Синтаксис модальных формул. Семантика Крипке: шкала, модель, истинность. Истинность модальной формулы в точке модели как игра (точнее, как наличие у одного из игроков выигрышной стратегии в описанной на лекции игре).
    Общезначимость формулы на шкале. Понятие логики шкалы. Постановка адачи «Логики кластеров» — установить включения и равенства между логиками шкал (конечных и бесконечных) с универсальным отношенем R = W × W. Логика одноточечной рефлексивной шкалы.
  2. 2018.09.21: Синтаксис модальных формул и семантика Крипке (повтор). Задача «Логики кластеров»: а) установлено включение между логиками; б) установлена строгость включений. Осталось: равенство логик любого бесконечного кластера; сходимость логик конечных кластеров к логике бесконечного кластера.
  3. 2018.09.28: Лемма. Логика всех конечных кластеров (то есть пересечение всех Ln, n∈N) содержится в логике любого бесконечного кластера. А значит, они равны. Следствие. Равны логики следующих классов шкал: (1) все конечные кластеры; (2) все бесконечные кластеры; (3) все кластеры; (4) один бесконечный кластер (любой мощности); (5) один счетный кластер.

    Определение: модальный морфизм (шкал и моделей).
    Без доказательства: если есть сюръективный модальный морфизм из шкалы F на шкалу F', то L(F) ⊆ L(F').
    Применение этого факта для короткого доказательства того, что Ln+1 ⊆ Ln.
    Модальный морфизм произвольной модели над бесконечным кластером НА модель над некоторым конечным кластером, согласованный с истинностью лишь первых s переменных. Как следствие, вышеуказанная лемма.

  4. 2018.10.05: Определения: истинность формулы в точке модели, в модели; общезначимость формулы в точке шкалы, в шкале.
    Определения: теория отмеченной модели, теория модели; логика отмеченной шкалы, логика шкалы.
    Определение: Модальный морфизм (напоминание).

    Лемма 1 (основная о морфизмах): в точке и в ее образе верны одни и те же модальные формулы.

    Следствие 1: без сюръективности так:
    (1) M,x ⊨ A <==> M',x' ⊨ A
    (2) M ⊨ A <== M' ⊨ A
    (3) F,x ⊨ A ==> F', x' ⊨ A
    (4) F ⊨ A и F' ⊨ A  — нет ни одной импликации.
    Если потребовать сюръективности f, то
    (2') M ⊨ A <==> M' ⊨ A
    (3') F,x ⊨ A ==> F',x' ⊨ A
    (4') F ⊨ A ==> F' ⊨ A.
    Никакие из оставшихся импликаций не верны (Упражнение: привести контрпримеры).

    Следствие 2. Аналог Следствия 1 в терминах теорий и логик.
    Определение: теория, нормальная теория, логика, нормальная логика.
    Лемма 2. (без доказательства):
    теория отмеченной модели — теория;
    теория модели — нормальная теория;
    логика отмеченной шкалы — логика;
    логика шкалы — нормальная логика.

    Лемма 3. Аналогичное утверждение для классов соответствующих структур.
    Вопрос на дом: перейдя к рассмотрению классов, получили ли мы новые теории и новые логики?

  5. 2018.10.12: Несвязная сумма моделей и шкал. Основная лемма. Следствие для теорий и логик.
    Лемма. а) Теория всякого класса моделей является теорией некоторой модели. (Для отмеченных моделей это не верно.)
    б) Логика всякого класса шкал является логикой некоторой шкалы. (Для отмеченных шкал это не верно — оставлено как задача.)
  6. 2018.10.19: Модальная эквивалентность (отмеченных) моделей или шкал. Включение теории (логики) одной структуры в теорию (логику) другой структуры. Лемма: если теория одной отмеченной модели содержится в теории другой отмеченной модели, то эти отмеченные модели модально эквивалентны.
    Порожденная подмодель, подшкала. Подмодель (подшкала), порожденная одной точкой или некоторым множеством точек. Основная лемма про порожденные подмодели. Следствие для теорий и логик.
    Логика одноточечной рефлексивной шкалы есть Triv. Логика одноточечной иррефлексивной шкалы есть Ver.
    Теорема Макинсона. Логика всякой шкалы содержится в логике Triv или Ver.
  7. 2018.10.26: Бисимуляция. Бисимуляционная эквивалентность отмеченных моделей. Основная лемма: бисимулирующие отмеченные модели модально эквивалентны.
    Глобальная бисимуляция между моделями, она влечет модальную эквивалентность моделей.
    Обратное утверждение неверно: Модальная эквивалентность (отмеченных моделей) не влечет бисимуляцию: контрпример (детали оставлены для самостоятельного продумывания).
    Обратное верно для конечных моделей и для моделей конечного ветвления (доказательство).
  8. 2018.11.02:
    Определение: теория, нормальная теория, логика, нормальная логика.
    Теорема корректности:
    а) теория отмеченной модели — теория;
    б) теория модели — нормальная теория;
    в) логика отмеченной шкалы — логика;
    г) логика шкалы — нормальная логика.
    Следствие. Аналогичное утверждение для классов соответствующих структур. (Доказательство тривиально, т.к. это пересечения теорий / логик из предыдущей теоремы, а замкнутость относительно правил вывода сохраняется при взятии произвольных пересечений.)
    Лемма. Эквивалентные определения полной по Крипке логики:
    1) L есть логика некоторого класса шкал;
    2) L есть логика класса Frames(L) всех своих шкал;
    3) L есть логика некоторой шкалы;
    4) L ⊢ A  ⇔  L ⊧ A; (одна импликация верна всегда)
    5) если A не выводится в L, то существует шкала F, в которой общезначима L, но не общезначима A.
  9. 2018.11.09: Лемма о корректности (еще раз): Пусть L=K⊕Г. Тогда если L ⊢ A, то в любой шкале, в которой общезначимо Г, общезначима и формула A.

    «Традиционные» модальные логики: модальные аксиомы сериальности D, рефлексивности T, симметричности B, транзитивности 4, евклидовости 5. Соответствующие им условия первого порядка на шкалы Крипке. Доказательство этого соответствия (для евклидовых шкал). Обсуждение, что в общем случае получается условие второго порядка.
    Имена традиционных логик. Теорема о корректности (еще раз формулировка):
    если S4 ⊢ A, то формула A общезначима на всех рефлексивных транзитивных шкалах.
    Наша задача — доказать обратное утверждение (полноту).

    Два эквивалентных определения (точек будущей канонической модели) для непротиворечивой (нормальной) логики или теории L:
    1) максимальные L-непротиворечивые множества формул (L-м.н.м.);
    2) непротиворечивые полные теории, содержащие L (L-п.н.т.).
    Лемма о пополнении. Если множество Г является L-непротиворечивым, то Г + А или Г + не-А является L-непротиворечивым.
    Лемма. Множество формул является L-м.н.м.  ⇔  оно является L-п.н.т.

  10. 2018.11.16: Каноническая модель (продолжение).
    Два эквивалентных определения: L-м.н.м. и L-п.н.т.
    Лемма Линденбаума: всякое L-непротиворечивое множество формул содержится в некотором L-м.н.м. (аналогично для L-п.н.т.).
    Лемма о М.Н.М.: принадлежность формул к L-м.н.м. согласована с булевыми связками.
    Определение канонической модели ML непротиворечивой нормальной логики (или более общо — нормальной теории).
    Лемма о канонической оценке: x ⊧ A  ⇔  A ∈ x. То есть Theory(ML,x) = x.
    Теорема о канонической модели: ML ⊧ A  ⇔  A ∈ L. То есть Theory(ML) = L.
    Следствия: теоремы о полноте (пока для теорий):
    Теорема 1. Всякая непротиворечивая теория является теорией некоторого класса моделей; более того, теорией одной модели; более того, модели мощности не более континуума. (а именно, она есть теория своей канонической модели)
    Теорема 2. Всякая синтаксически полная непротиворечивая теория является теорией некоторой отмеченной модели (опять мощности не более континуума). (а именно, она есть одна из точек канонической модели логики K)
    Теорема 3. Всякая непротиворечивая теория является теорией некоторого класса отмеченных моделей. (а именно, теорией совокупности точек из канонической модели логики K, содержащих данную теорию).

    Дальнейший план (может измениться):
    Канонические логики, канонические формулы.
    Каноничность => Сильная полнота => полнота.
    Каноничность (i,j,m,n)-формул.
    Примеры неканонических, не сильно полных (но полных) логик.
    Неполная логика (Benton или Magari).
    Фильтрация. Финитная аппроксимируемость.

  11. 2018.11.23:
  12. 2018.11.30:
  13. 2018.12.07:
  14. 2018.12.14:

Модальная логика
(годовой спецкурс, 2016—2017)
с.н.с. Е.Е.Золин

Конспект лекций: [ pdf ] (только новое по сравнению с конспектами прошлых лет)
Про ультра-расширение и ТГТ: pdf ]
Вопросы к экзамену: [ pdf ]
Задачи к экзамену: [ pdf ]

Слайды-обзор критериев: [ rus ] [ eng ]

Литература

  1. Valentin Goranko & Martin Otto «Model Theory of Modal Logic», Chapter 5 of Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, Frank Wolter, editors. Elsevier, 2007. [доступно в сети]
  2. Johan van Benthem «Modal Logic for Open Minds», CSLI Lecture Notes, volume 199, 2000. [доступно в сети]
  3. Krister Segerberg «An Essay in Classical Modal Logic», 1971. (Revised version of his PhD Thesis) [ pdf ] (typeset by me, incomplete)
  4. Melvin Fitting «Proof Methods for Modal and Intuitionistic Logics», Synthese Library, volume 169, 1983. [доступно в сети]

Модели неклассических логик
(годовой спецкурс, 2015—2016)
Е.Е.Золин, И.Б.Шапировский

Конспект лекций: [ pdf ] (неоконченный)

Отдельный текст pdf ] покрывает следующие темы (но отличается от изложения на лекциях):
- операции на шкалах и моделях, теоремы о сохранении;
- фильтры и ультрафильтры, в том числе счетно-неполные;
- ультрапроизведения и теорема Лося;
- ультрарасширение модели Крипке;
- модально компактные классы шкал;
- насыщенные модели первого порядка;
- модально насыщенные модели Крипке;
- теорема Гольдблатта-Томасона.

Литература

  1. Modal Logic — Patrick Blackburn, Maarten de Rijke, and Yde Venema. Cambridge Tracts in Theoretical Computer Science, Volume 53, Cambridge University Press, 2001. [Доступно в сети]
  2. Modal Logic — Alexander Chagrov and Michael Zakharyaschev. Oxford Logic Guides, Volume 35, Oxford University Press, 1997. [Доступно в сети]
  3. Logics of Time and Computation, 2nd Edition — Robert Goldblatt. CSLI Lecture Notes, No. 7. CSLI Publications, 1992. [Доступно в сети]

Модальная логика и ее приложения
(годовой спецкурс, 2014—2015)
Е.Е.Золин, И.Б.Шапировский

Программа курса: [ pdf ]

Конспект лекций: [ pdf ] (неоконченный)

Литература

    Часть 1. Синтаксис и семантика модальной логики. Операции на шкалах и моделях. Модальная определимость. Модальные исчисления. Каноническая модель. Полные по Крипке логики. Разрешимость минимальной модальной логики. Кодирование проблемы домино и неразрешимые логики.
  1. Modal Logic — Patrick Blackburn, Maarten de Rijke, and Yde Venema. Cambridge Tracts in Theoretical Computer Science, Volume 53, Cambridge University Press, 2001. [Доступно в сети]
  2. Modal Logic — Alexander Chagrov and Michael Zakharyaschev. Oxford Logic Guides, Volume 35, Oxford University Press, 1997. [Доступно в сети]
    Часть 2. Расширенные модальные языки: Обратные модальности, временная логика (tense logic). Универсальная модальность. Модальность транзитивного замыкания.
  3. Logics of Time and Computation, 2nd Edition — Robert Goldblatt. CSLI Lecture Notes, No. 7. CSLI Publications, 1992. [Доступно в сети]
  4. Элементарное доказательство полноты логики K, расширенной модальностью транзитивного замыкания — Е.Е.Золин, 2015. [ pdf ]
    Часть 3. Дескрипционная логика.
  5. Е.Е.Золин. Дескрипционная логика (конспект лекций годового спецкурса), 2013.
  6. The Description Logic Handbook: Theory, Implementation and Applications, 2nd Edition — Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. Cambridge University Press, 2007. [Доступно в сети]
  7. A Description Logic Primer — Markus Krotzsch, Frantisek Simancik, Ian Horrocks, 2013. Available at arXiv:1201.4089.
    Часть 4. Пропозициональная динамическая логика PDL.
  8. Logics of Time and Computation, 2nd Edition — Robert Goldblatt. CSLI Lecture Notes, No. 7. CSLI Publications, 1992. [Доступно в сети]
  9. Dynamic Logic — David Harel, Dexter Kozen, Jerzy Tiuryn. Foundations of Computing Series. The MIT Press, 2000. [Доступно в сети]
  10. A Concise Introduction to Propositional Dynamic Logic — Krister Segerberg, 1993 (short book). [ pdf ]
  11. An elementary proof of the completeness of PDL — Dexter Kozen, Rohit Parikh. Theoretical Computer Science, 1981, vol.14, pp. 113-118. [ pdf ]
    Часть 4. Логики деревьев вычислений (CTL, LTL). Верификация моделей (model checking).
  12. Верификация моделей программ: model checking — Э.М.Кларк мл., Д.Пелед, О.Грамберг. Переводчики: В.Захаров, Р.Кончаков, Д.Царьков, Р.Смелянский. Издательство МЦНМО, 2002. [Доступно в сети]