Назад

Модальная логика
(годовой спецкурс, 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, содержащих данную теорию).
  11. 2018.11.23: Определение: каноническая логика.
    Лемма. Всякая каноническая логика полна по Крипке.
    Определение: Сильно полная логика.
    Лемма. Всякая каноническая логика сильно полна по Крипке.
    Определение: каноническая формула A — означает, что логика K⊕A является канонической.
    Лемма. Если L⊆L', то каноническая модель логики L' является порожденной подмоделью в канонической модели логики L.
    Лемма о канонических формулах. Всякая каноническая формула общезначима на канонической шкале FL любой (а не только наименьшей) нормальной логики L, содержащей данную формулу.
    Следствие. Всякая нормальная логика L=K⊕Γ, аксиоматизированная каноническими формулами, является канонической (а значит, сильно полной и полной).

    Напоминание 5 аксиом «традиционных» модальных логик.
    Модальная (i,j,m,n)-формула. Соответствующее ей на шкалах Крипке (i,j,m,n)-условие первого порядка. Лемма об их соответствии друг другу.
    Лемма. Каноничность всякой (i,j,m,n)-формулы.
    Теорема. Для всякого множества (i,j,m,n)-формул Γ, логика L=K⊕Γ является канонической (а значит, сильно полной и полной).

  12. 2018.11.30: Определения: конечно аксиоматизируемая [К.А.] (нормальная) логика; разрешимая логика; перечислимая логика.
    Лемма. Всякая конечно аксиоматизируемая логика перечислима.
    Определение. Финитно аппроксимируемая [Ф.А.] логика (или иначе — логика, полная относительно конечных шкал).
    Теорема Харропа. Если логика К.А. и Ф.А., то она разрешима.

    Определение. Модель N является (некоторой!) фильтрацией модели M через множество формул Ф (при условии, что Ф замкнуто относительно подформул).
    Более интуитивная терминология — фильтрацией можно было бы называть не саму модель N, а процесс / способ построения N по M и Ф; а модель N называть результатом фильтрации (или фильтратом :) модели M через Ф.
    Запись условий на отношение R в терминах Rmin и Rmax
    Данное определение — узкое, в нем факторизуют W по Ф и максимальное отношение Rmax строят тоже по Ф. На самом деле, достаточно, чтобы первое множество лишь содержало второе (такое определение будет позже, иначе мы не сможем доказать Ф.А. для некоторых «традиционных» логик).
    Лемма о фильтрации. В точке исходной модели M и в соответствующей точке отфильтрованной модели истинны одни и те же формулы из Ф.

    L-моделью называем модель M=(F,V), в шкале F которой общезначима логика L.
    Определение (одно из возможных). Говорим, что логика L допускает фильтрацию [Д.Ф.] (или лучше — фильтруема), если для всякой L-модели M и всякого к.з.о.п. (конечного замкнутого относительно подформул) множества формул Ф существует L-модель N, являющаяся фильтрацией N модели M через Ф.
    Лемма. Если логика L полна по Крипке и Д.Ф., то она Ф.А.
    Теорема. Логика K — Д.Ф. (а значит, она Ф.А. и разрешима).

  13. 2018.12.07: Фильтруемость «традиционных» логик: сериальность, рефлексивность, симметричность. С транзитивностью чуть посложнее: два способа (фильтрация Леммона и транзитивное замыкание минимального отношения). С евклидовостью еще чуть сложнее — нужно расширить понятие фильтрации, чем и займёмся.

    Более широкое определение фильтрации: фильтрация модели M через множество Ф, сохраняя множество Г. Отвечающее ему определение фильтруемости логики (другой термин — логика допускает фильтрацию, Д.Ф.). Опять полнота по Крипке и Д.Ф. влекут Ф.А.

    Фильтруемость логики K + n-транзитивность. Фильтруемость логики K5 (на лекции попытка упрощенного доказательства для K5 оказалась неверной; существенно доработанное доказательство набрано в конспектах).

  14. 2018.12.14: Лемма. Если логика L строго содержится в логике L', но Frames(L)=Frames(L'), то логика L не полна по Крипке.

    Примеры (без доказательства) двух неполных по Крипке логик: Benton и Magari.

    Пример полной, но не сильно полной (и, следовательно, не канонической) логики — GL:

    Логика Гёделя – Лёба GL. Описание класса шкал этой логики — транзитивные обратно фундированные шкалы.
    Два эквивалентных, по модулю аксиомы выбора, определения обратно фундированных шкал:
    1) в каждом непустом подмножестве существует R-максимальный элемент;
    2) не существует бесконечно возрастающей R-цепи x0Rx1Rx2R... (не обязательно попарно различных элементов).
    Класс конечных шкал логики GL — иррефлексивные транзитивные шкалы.

    Лемма. Логика GL не является сильно полной.
    Лемма. Логика GL — не фильтруемая (не Д.Ф.) в нашем смысле: шкала (N,>) является GL-шкалой, но если ее фильтровать, то непременно будет цикл.
    Теорема. Логика GL полна относительно конечных шкал (т.е. Ф.А.).
    А так как она конечно аксиоматизируема, то, следовательно, она разрешима.

весенний семестр 2019 года

  1. 2019.02.15: Некоторые свойства конечных моделей Крипке:
    Теорема 1. Пусть M и M' — конечные модели, модально эквивалентные M≡M'. Тогда для каждой точки a из M найдется модально эквивалентная точка a' из M', и наоборот.
    Напоминание: общезначимость формулы □p→p на шкале F=(W,R) равносильна тому, что R рефлексивно.
    Наблюдение: из того, что в модели M истинна формула □p→p, не следует рефлексивность отношения R. Более того, из того, что в модели M истинна схема рефлексивности, то есть истинны формулы □A→A для всех формул A, не следует рефлексивность отношения R! Контрпример: модель из двух точек, видящих друг друга, и одинаково оценивающих всякую переменную.
    Оказывается, если добавить еще одно свойство модели, то утверждение станет верным: модель M называется модально различимой, если никакие две различные точки в ней не являются модально эквивалентными.
    Теорема 2. Пусть M=(F,V) — конечная модально различимая модель, и пусть M⊧ A*, то есть в M истинны все подстановочные примеры формулы A. Тогда формула A общезначима на шкале F.

  2. 2019.02.22: Компактные модели Крипке: эквивалентные определения (3 или 4).
    Всякая конечная модель компактна. Для компактных моделей тоже верна Теорема 1 из предыдущей лекции.

  3. 2019.03.01: Насыщенные модели Крипке.
    Множество точек X⊆W модели Крипке M=(W,R,V) называется компактным, если ... (несколько эквивалентных определений).
    Модель называется компактной, если множество W компактно.
    Модель называется насыщенной, если для каждой ее точки a множество последователей R(a) компактно.
    Следствия из определений: всякая конечная модель — компактна, всякая модель конечного ветвления — насыщенна.
    Теорема. Если M и M' — насыщенные модели, то из (M,a)≡(M',a') следует наличие бисимуляции между (M,a) и (M',a').
    Теорема. Если M и M' — компактные и насыщенные модели, то из M≡M' следует наличие глобальной бисимуляции между M и M'.

  4. 2019.03.15: Свойства логик двух похожих друг на друга шкал могут кардинально различаться:
    Теорема 1. Логика бесконечного рефлексивного кластера (W,W×W) равна S5.
    Логика L называется n-аксиоматизируемой, если она аксиоматизируется некоторым множеством формул от переменных {p1,...,pn}.
    Теорема 2. (Шапировский, 2005?) Логика бесконечного иррефлексивного кластера (W,≠) не является n-аксиоматизируемой ни для какого n. В частности, она не является конечно аксиоматизируемой.
    Лемма (Шехтман, Скворцов, Максимова, 197x). Пусть логика L такова, что существуют шкалы F и F', на которых общезначимы одни и те же формулы от переменных {p1,...,pn} (обозначение F≡nF'), и при этом логика L общезначима на F, но не на F'. Тогда логика L не является n-аксиоматизируемой.

  5. 2019.03.22: Эквивалентная формулировка Леммы из предыдущей лекции:
    Лемма. Если логика L является n-аксиоматизируемой, то класс ее шкал Frames(L) замкнут относительно ≡n.
    Окончание доказательства теоремы 2 из предыдущей лекции — доказательство того, что F≡nF'.
    Формулы Янкова-Файна. Основная лемма: Формула Я(F,a) выполнима в корне a' транзитивной шкалы F' <==> существует сюръективный p-морфизм из (F', a') на (F,a).

  6. 2019.03.29: Напоминание понятий: несвязная сумма, порожденная подмодель, p-морфизм.
    Лемма о накрытии: Всякая шкала является p-морфным образом несвязной суммы всех своих корневых подшкал.
    Применение формул Янкова-Файна — аналог теоремы Гольдблатта-Томасона для конечных транзитивных шкал:
    Теорема. Класс конечных транзитивных шкал модально определим (некоторым множеством модальных формул) <==> он замкнут относительно операций взятия p-морфизмов, порожденных подшкал и (конечных) несвязных сумм.
    Каков критерий модальной определимости класса транзитивных шкал одной модальной формулой? (быть может, это открытый вопрос?)

  7. 2019.04.05: Интерполяционная теорема Крейга для логик K, KT, K4, S4.
    Доказательство (автор - Сморинский).

  8. 2019.04.12: Конечные бисимуляционные игры. Определение игры Game[(M,a),(M',a')]. Множество переменных конечно!
    Существование выигрышной стратегии у одного из игроков (без док-ва).
    Теорема 1: (M,a)≡(M',a') <==> у игрока P2 есть выигрышная стратегия в Game[(M,a),(M',a')]. (пока без док-ва)
    Модальная глубина модальной формулы. Эквивалентность ≡n. Игра Gamen[(M,a),(M',a')].
    Теорема 2: (M,a)≡n(M',a') <==> у игрока P2 есть выигрышная стратегия в Gamen[(M,a),(M',a')]. (пока без док-ва)
    Пример: две модели: (M,a) --- из a идут цепи длины 1, 2, 3, ...; (M',a') --- из a идут те же цепи, плюс одна бесконечная цепь. Предъявление выигрышной стратегии для игрока P2.
    Пример, показывающий, что если множество переменных бесконечно, то перестает быть верной Теорема 1, и более точно --- имликация => в Теореме 2 для n=1 (импликация <= останется верной).

  9. 2019.04.19: Доказательство Теоремы 2.
    Бесконечная бисимуляционная игра --- определение.
    Теорема 3 об игровой характеризации бисимуляции (пока без доказательства).

  10. 2019.04.26: Доказательство Теоремы 3.
    Инфинитарные модальные языки MLϰ с конъюнкциями по множествам формул мощности <ϰ.
    Неограниченный инфинитарный модальный язык ML (с конъюнкциями по любым множествам формул).
    Лемма. Совокупность формул языка ML является (не множеством, а) собственным классом.
    Теорема. Модальная эквивалентность в языке ML двух отмеченных моделей равносильна их бисимуляционной эквивалентности (некорректное и корректное доказательства).
    Следствие. Бесконечная бисимуляционная игра является игровой характеризацией модальной эквивалентности в языке ML.
    Вопрос (на который лектору неизвестен ответ): есть ли игровая характеризация модальной эквивалентности отмеченных моделей в языке MLϰ?

  11. 2019.05.10: Инфинитарный модальный язык MLϰ. Определение (1) понятия ϰ-компактного множества точек X модели Крипке.
    Вопрос (на который лектору неизвестен ответ): как соотносятся друг с другом понятия ϰ-компактности множества X? Заведомо не могут сужаться, а вот расширяются ли или находятся в общем положении?
    Лемма. Всякое множество X мощности |X|<ϰ является κ-компактным.
    Определения κ-компактной и ϰ-насыщенной модели.
    Теорема. Всякая модель мощности меньше ϰ является ϰ-компактной.
    Теорема. Всякая модель ветвления менее ϰ является ϰ-насыщенной.
    Теорема. На κ-насыщенных моделях модальная ϰ-эквивалентность точек совпадает с бисимуляционной эквивалентностью.
    Теорема. На ϰ-компактных ϰ-насыщенных моделях модальная ϰ-эквивалентность совпадает с глобальной бисимуляционной эквивалентность.
    Определение (1') понятия ϰ-компактного множества точек X модели Крипке M.
    Доказательство эквивалентности определений (1) и (1').

  12. 2019.05.17: Логика транзитивного замыкания K+. Семантика; эквивалентные определения транзитивного замыкания. Аксиомы Сегерберга. Описание класса шкал, задаваемого аксиомами Сегерберга. Теорема о полноте K+ относительно конечных шкал. Замечание: сильной полноты нет, т.к. логика некомпактна (пример). Доказательство теоремы - замыкание Фишера-Ладнера. конечная каноническая модель; минимальные и максимальные отношения (аналоги фильтрации), убывающие и возрастающие шкалы с двумя отношениями.