Назад

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

Краткое содержание лекций

ОСЕНЬ 2019

  1. 2019.09.20: Введение. Различные виды модальностей (необходимо - возможно; всегда будет - иногда будет; доказуемо; знает, что).
    Синтаксис модальных формул. Семантика Крипке. Истинность в модели, общезначимость на шкале.
    Лемма. F ⊧ □p→p ⇔ отношение R рефлексивно.
    Задача. Пусть Ln — логика иррефлексивного цикла из n точек. Установить включения между этими логиками.

  2. 2019.09.27: Решение задачи про логики конечных циклов: Ln ⊂ Lm <==> n делится на m.
    Развитие задачи: пересечение логик всех конечных циклов. Утверждается, что оно равно логике целых чисел L(Z) (с отношением «следующее целое число»). Доказательство простого включения: L(Z) содержится в логике каждого цикла.

  3. 2019.10.04: Для доказательства оставшегося включения вводим понятие: модальная глубина d(A) формулы A.
    Мы опишем три преобразования моделей Крипке, сохраняющих истинность формул в точке: «стрижка» (уменьшение глубины, то есть длины путей); «распутывание» (превращение модели в дерево с корнем в данной точке); «прореживание» (уменьшение количества исходящих ребер).
    (1) Определение. Если M=(W,R,V) модель, то конус Mxn с вершиной x глубины n — это совокупность точек, достижимых из x не более чем за n шагов.
    Лемма. M,x ⊧ A <==> Mxn,x ⊧ A, для всякой формулы A глубины d(A)≤n.
    В задаче доказываем оставшееся включение: если формула A глубины n=d(A) опровергается на Z, то она опровергается и на цикле длины ≥n.
    Определение. Конус Mx с вершиной x — совокупность точек, достижимых из x за некоторое конечное число шагов. Другое название: подмодель, порожденная точкой x.
    Следствие. M,x ⊧ A <==> Mx,x ⊧ A, для всякой формулы A.
    (2) Определение. Развертка модели (множество всех конечных путей, выходящих из данной точки). Формулировка Леммы: в точке x модели M истинны те же формулы, что и в этой же точке в развертке.

  4. 2019.10.11: Напоминание определения развертки. Доказательство леммы.
    (3) Определение. Модель имеет ветвление ≤m, если из каждой точки выходит не более m ребер.
    Лемма. Всякая выполнимая формула A выполнима в модели ветвления ≤ m=число боксов в A.

  5. 2019.10.18: Объединяем полученные результаты: Всякая выполнимая формула выполнима в корне некоторого конечного дерева.
    Следствия: Проблема выполнимости модальных формул разрешима. Проблема общезначимости модальных формул разрешима.
    Исчисление К. Определение подстановки формул вместо переменных. Формулировка двух исчислений для К: одно с аксиомами и тремя правилами вывода (MP), (Nec), (Sub), другое со схемами аксиом и двумя правилами (MP) и (Nec). Доказательство эквивалентности двух исчислений.
    Определение нормальной логики. Обозначение K⊕Γ — нормальная логика, аксиоматизированная множеством формул Γ. Определение конечно аксиоматизируемой логики.
    Критерий Тарского конечной аксиоматизируемости. Нормальная логика конечно аксиоматизируема <==> она не представима в виде объединения башни строго возрастающих (нормальных) логик.

  6. 2019.10.25: Выводимые в К формулы. Общезначимые формулы.
    Определения: теория (отмеченной) модели, логика (отмеченной) шкалы.
    Теорема о корректности:
    а) Th(M,x) содержит все аксиомы логики К.
    б) Th(M,x) замкнуто по правилу MP,
    в) Th(M) замкнуто по правилу Nec,
    г) Logic(F,x) замкнуто по правилу Sub.
    Определение: теория, нормальная теория, логика, нормальная логика.
    Следствие.
    а) Th(M,x) — теория.
    б) Th(M) — нормальная теория
    в) Logic(F,x) — логика.
    г) Logic(F) — нормальная логика.
    Следствие: аналогичное верно для классов соответствующих структур:
    а) Теория некоторого класса отмеченных моделей — теория.
    б) Теория некоторого класса моделей — нормальная теория.
    в) Логика некоторого класса отмеченных шкал — логика.
    г) Логика некоторого класса шкал — нормальная логика.
    Определения: локальная и глобальная выводимость формулы А из множества гипотез Г в данной логике L.
    Определения: локальное и глобальное следование формулы А из множества гипотез Г над данной логикой L.
    Следствия: из локальной (глобальной) выводимости следует локальное (глобальное) следование.
    Если верна обратная импликация, то логика называется сильно (локально / глобально) полной (по Крипке): СЛП и СГП.

  7. 2019.11.01: Локальная и глобальная выводимость формулы А из множества гипотез Г в данной логике L. Основные факты:
    Компактность. Теорема о дедукции.
    Сводимость локальной к глобальной выводимости и наоборот.
    Над K4 теорема о дедукции проще, над S4 еще проще.

  8. 2019.11.08: Локальное и глобальное следование формулы А из множества гипотез Г над данной логикой L. Основные факты: компактность не всегда имеет место; теорема о дедукции (лишь для локального). Сводимость локального к глобальному следованию и наоборот.
    Определения: локальная полнота логики, глобальная полнота логики, сильная (локальная / глобальная) полнота логики.
    Теорема. СЛП = СГП.
    Кратко: полнота относительно класса конечных L-шкал: ПОКШ, ГПОКШ, СПОКШ.

  9. 2019.11.15: Каноническая модель. Определения L-м.н.м. (максимальных L-непротиворечивых множеств) и L-п.н.т. (синтаксически полных синтаксически непротиворечивых теорий, содержащих L). Их эквивалентность.
    Лемма о пополнении. Если множество Г является L-непротиворечивым, то Г + А или Г + не-А является L-непротиворечивым.
    Лемма. Множество формул является L-м.н.м.  ⇔  оно является L-п.н.т.
    Лемма Линденбаума: всякое L-непротиворечивое множество формул содержится в некотором L-м.н.м.
    Лемма о М.Н.М.: принадлежность формул к L-м.н.м. согласована с булевыми связками.
    Определение канонической модели ML непротиворечивой нормальной логики (или более общо — нормальной теории).
    Лемма о канонической оценке: x ⊧ A  ⇔  A ∈ x. То есть Theory(ML,x) = x.

  10. 2019.11.22: Напоминание: каноническая модель ML непротиворечивой нормальной логики (или теории) L.
    Теорема о канонической модели: ML ⊧ A  ⇔  A ∈ L. То есть Theory(ML) = L.
    Определение. Каноническая логика, ее сильная полнота.
    Теорема 1. Всякая непротиворечивая полная теория есть теория некоторой отмеченной модели.
    Теорема 2. Всякая непротиворечивая нормальная теория есть теория некоторой модели.
    Теорема 1'. Всякая непротиворечивая теория есть теория некоторого класса отмеченных моделей.
    Теорема 2'. Всякая непротиворечивая нормальная теория есть теория некоторого класса моделей (состоящего даже из одной модели).
    Для логик и нормальных логик аналогичные утверждения не всегда верны (существуют неполные по Крипке логики).
    Определение. Каноническая формула.
    Лемма о канонических формулах: Каноническая формула общезначима на канонической шкале любой нормальной логики, содержащей эту формулу (пока без док-ва).
    Теорема. Логика, аксиоматизированная каноническими формулами, является канонической (а значит, сильно полной).
    (i,j,m,n)-формулы. Их каноничность (без доказательства, см. конспект 2014-2015 года).
    Формулы Height<n и Width<n. Задаваемые ими свойства шкал (задача). Их каноничность (пока без док-ва).

  11. 2019.11.29: Порожденные подмодели и подшкалы. Сохранение общезначимости модальных формул при переходе к порожденной подшкале.
    Лемма. Если L⊆L', то каноническая модель логики L' является порожденной подмоделью в канонической модели логики L.
    Лемма о канонических формулах. Всякая каноническая формула общезначима на канонической шкале FL любой (а не только наименьшей) нормальной логики L, содержащей данную формулу.
    Теорема. Всякая нормальная логика L=K⊕Γ, аксиоматизированная каноническими формулами, является канонической (а значит, сильно полной и полной).

    Определение. Модально различимая модель.
    Каноническая модель — модально различимая.
    Лемма. Пусть M — модально различимая модель. Тогда для любых n попарно различных точек x1...xn существуют n модальных формул B1...Bn, такие что xi ⊧ Bj   <==>   i = j.
    Лемма. Пусть M=(F,V) — конечная модально различимая модель, и пусть M⊧ A*, то есть в M истинны все подстановочные примеры формулы A. Тогда F⊧ A.
    Пример конечной, но не модально различимой модели, в которой заключение неверно (две точки, видящие друг друга, с одинаковой оценкой переменных; формула рефлексивности).
    Задача. Придумать модально различимую, но бесконечную модель, тоже являющуюся контрпримером к лемме (то есть в которой истинны все подстановочные примеры формулы рефлексивности, но формула рефлексивности не общезначима на шкале, ибо шкала не (во всех точках) рефлексивна).


  12. 2019.12.06: Формулы Height<n и Width<n. Условие на класс шкал, которое они выражают.
    Определение стабильных формул.
    Лемма. Стабильная формула, общезначимая хотя бы на одной шкале, => каноническая.
    Формулы Height<n и Width<n стабильные. А значит, канонические.
    Критерий табличности нормальной логики.

  13. 2019.12.13: Табличная логика. Ее разрешимость.
    Лемма. Табличная логика имеет конечное число расширений, и все они табличны.
    Лемма (о пустом интервале логик). Если L1 и L2 — нормальные логики, L1 ⊂ L2, и между ними нет других нормальных логик, то L2 конечно аксиоматизируется над L1.
    Конечная аксиоматизируемость всякой табличной модальной логики.

    Полнота (локальная, глобальная, сильная) относительно конечных шкал. Модально компактные классы шкал. Некомпатность класса всех конечных шкал. Связь сильной полноты логики относительно класса шкал с модальной компактностью этого класса.
    Теорема. Сильная полнота логики относительно конечных шкал <==> табличность логики.

ВЕСНА 2020

  1. 2020.02.14: Общезначимость модальной формулы на шкале Крипке. Два направления исследований: 1) берется модальная формула и изучается класс шкал (всех или конечных), которые она описывает: является ли он первопорядковым? можно ли по модальной формуле построить первопорядковое условие алгоритмом? и т.д. 2) берется шкала; требуется выяснить, что про нее может сказать модальный язык: как аксиоматизировать логику этой шкалы? можно ли эту аксиоматику построить по конечной шкале алгоритмом?

    Круг вопросов, относящихся к первому подходу:
    Модальные формулы, выражающие рефлексивность, симметричность, транзитивность.
    Лемма. F ⊧ p → ◊□ p ⇔ некоторое условие первого порядка на отношение R (найдите его). Это условие использует равенство. Можно ли выразить то же условие, не используя равенство? (вопрос оставлен без ответа)
    Общезначимость модальной формулы на шкале в общем случае отвечает некоторому условию 2-го порядка на бинарное отношение R.
    Всякая ли формула вида p → Ц p, где Ц — произвольная цепочка боксов и ромбов, будет выражать условие 1-го порядка? Какие из них можно будет записать, не используя равенство? (вопросы оставлены на размышление)
    Модальная формула может соответствовать (на шкалах) замкнутой формуле первого поряка (то есть глобально), а может соответствовать (на отмеченных шкалах) формуле первого порядка с одной свободной переменной (то есть локально). Из локального соответствия следует глобальное, но не наоборот (пример не приводился).
    Общие факты:
    (1) Множество модальных формул, выражающих условие 1-го порядка (на шкалах), неразрешимо (Чагрова). Аналогично на не более чем счетных шкалах, на конечных шкалах.
    (1') Не существует алгоритма, который по модальной формуле строит соответствующую ей замкнутую формулу 1-го порядка, если она существует, и выдает «Нет» в противном случае.
    (2) Не существует алгоритма, который по модальной формуле и замкнутой формуле первого порядка проверяет, что они соответствуют друг другу (на шкалах).
    (3) Не существует алгоритма, который по двум модальным формулам выясняет, задают ли они один и тот же класс шкал.
    Модальная формула, задающая не первопорядковый класс шкал, вполне может задавать первопорядковый класс конечных шкал. Пример: формула Лёба □(□p→p)→□p задает класс транзитивных шкал без бесконечно возрастающих цепей (условие 2-го порядка), но на конечных шкалах это вырождается в условие транзитивности и иррефлексивности (условие 1-го порядка).

    Круг вопросов, относящихся ко второму подходу:
    Рассматриваем двухточечные шкалы Крипке (изучались 4 шкалы F1, F2, F3, F4, где есть стрелка из a в b, но не наоборот). Будут ли их логики совпадать? Будут ли между этими логиками какие-либо включения? Были выписаны формулы, отличающие каждую из 4 шкал от других, за исключением одной пары шкал (оставлено на дом). На дом: нарисовать остальные 3 шкалы (где есть стрелка из a в b и обратная), найти формулы, показывающие, что среди логик всех 7 шкал нет никаких включений.
    Обозначение F⊑G означает: для каждой формулы A если F⊧A, то G⊧A.
    Вопрос. Существует ли алгоритм, который по двум конечным шкалам F и G выясняет, что F⊑G?
    Задача*. Найти формулу, аксиоматизирующую логику каждой из этих двухточечных шкал.
    Известно, что для каждой конечной шкалы F существует модальная формула A, которая аксиоматизирует логику этой шкалы: Logic(F)=K⊕A.
    Вопросы. Существует ли алгоритм, который по конечной шкале F строит ее аксиому A? Какова сложность этого алгоритма? Как завивит длина формулы |A| от размера шкалы |F|? Сколько минимально требуется переменных Var(A) в зависимости от размера шкалы |F|? И будет ли формула с наименьшим числом переменных наикратчайшей аксиомой логики Logic(F), а алгоритм построения такой аксиомы наипростейшим?


  2. 2020.02.21: Аксиомы логик S4 и S5. Обозначим двухточечную шкалу F4=({a,b},R), где aRa, bRb, aRb.
    Задача*. S4⊕A=S5 ⇔ A∈S5 и A не общезначима на двухточечной шкале F4.
    Этот результат вытекает из следующей теоремы:
    Теорема (Splitting). Для всякой логики вида L=S4⊕A, где A — произвольная формула, имеет место ровно одна из двух возможностей:
    S5 ⊆ L либо L ⊆ Logic(F4).
    Эту теорему записывают кратко: S4/F4=S5. Есть много подобных результатов.
    Как по конечной рефлексивной транзитивной шкале F найти логику S4/F? Можно ли наоборот, по произвольному расширению L логики S4 предъявить (конечную рефлексивную транзитивную) шкалу F, такую что S4/F=L?
    Для сравнения приведем аналогичный результат для интуиционистской Int и классической CL логик высказываний:
    Теорема (Янков). Int+A=CL ⇔ A∈CL и A не общезначима на двухточечной шкале F4.
    Здесь используется семантика Крипке для интуиционистских пропозициональных формул.

    §1. p-морфизм (модальный морфизм)
    Определение p-морфзима шкал и моделей. Сюръективный p-морфизм h:F↠F'.
    Обозначение F↠F' (шкала F' является p-морфным образом шкалы).
    Теорема 1. (a) Пусть h — p-морфизм из M в M'. Тогда для любой модальной формулы А имеем: M,x⊧A ⇔ M',h(x)⊧A.
    (b) Если F↠F', то F⊑F'.

    §2. Порожденная подшкала
    Определение порожденной подшкалы и подмодели.
    Примеры: подшкала, порожденная множеством X⊆W, точкой a∈W. Последняя обозначается Fa.
    Если Fa=F, то F называется конусом с вершиной a.
    Теорема 2. (a) Пусть M' — порожденная подмодель модели M и x∈W'. Тогда для любой формулы A имеем: M,x⊧A ⇔ M',x⊧A.
    (b) Если F'↪F, то F⊑F'.
    Упражнение 1. Логика шкалы равна логике всех ее конусов.
    Упражнение 2. Если логика L полна (относительно некоторого класса шкал), то она полна относительно некоторого класса конусов.

    §3. Субредукция шкал
    Определение. Говорим, что имеется субредукция шкалы F на шкалу G (и пишем F↣G), если G является p-морфным образом некоторой порожденной подшкалы шкалы F, то есть существует F'↪F, такая что F'↠G.
    Можно считать, что это частичный (то есть не обязательно всюду определенный) p-морфизм из F на G (его область определения есть шкала F').
    Теорема 3. Если F↣G, то F⊑G.
    Вопрос. На каком классе шкал (конечных) имеет место обратная импликация? Мы увидим, что на конечных конусах это верно. Более общо, это верно, если G – конечный конус, а F – конечная шкала.

    Установить для двухточечных шкал F1, F2, F3, F4, рассмотренных ранее, и одноточечных шкал G0 (иррефлексивной) и G1 (рефлексивной), является ли Gj p-морфным образом каких Fi, является ли Gj порожденной подшкалой каких Fi, является ли Gj субредуктом каких Fi. Параллельно выяснить включения логик Fi⊑Gj. Тем самым выяснить, субредукция покрыла все включения логик?

  3. 2020.02.28: Логики Triv и Ver.
    Лемма 1. Следующие три условия эквивалентны для любой формулы A:
    (1) Формула A общезначима на одноточечной рефлексивной шкале F1.
    (2) Формула A при стирании всех □ превращается в тавтологию.
    (3) Формула A принадлежит логике Triv.
    Лемма 2. Следующие три условия эквивалентны для любой формулы A:
    (1) Формула A общезначима на одноточечной иррефлексивной шкале F0.
    (2) Формула A при замене всех (достаточно только внешних) □ на T превращается в тавтологию.
    (3) Формула A принадлежит логике Ver.
    Слабая теорема Макинсона. Логика всякой шкалы Logic(F) содержится в Triv или Ver.
    Теорема Макинсона. Всякая непротиворечивая нормальная логика содержится в Triv или Ver.
    Следствие 1. Всякая непротиворечивая нормальная логик общезначима хотя бы на одной шкале.
    Для полимодальных логик это не верно (и как следствие, нет аналога теоремы Макинсона).
    Следствие 2. Проблема «по модальной формуле A выяснить, является ли нормальная логика K⊕A непротиворечивой» алгоритмически разрешима.
    (Достаточно проверить, содержится ли эта логика (то есть лежит ли формула A) в логике Triv или Ver.)

  4. 2020.03.06: Характеристическая формула конечного конуса (шкалы, порожденной точкой).
    Теорема 1. Если F - конечный конус, G - конечная шкала (чуть более общо, шкала конечной глубины), причем d=depth(G), то обозначив через χd(F) характеристическую формулу глубины d шкалы F, следующие условия эквивалентны:
    (1) G ↣ F;
    (2) Logic(G) ⊆ Logic(F);
    (3) на шкале G не общезначима формула χd(F).
    Лемма 1. Биективный p-морфизм шкал является изоморфизмом шкал.
    Теорема 2. Если логики двух конечных конусов равны, то эти конусы изоморфны.
    Теорема 3. У двух неизоморфных конечных конусов одного размера логики не содержатся друг в друге.

  5. 2020.03.13: Логика шкалы равна пересечению логик всех ее конусов.
    Для всяких конечных шкал G и F имеет место эквивалентность: Logic(G) ⊆ Logic(F) <==> каждый конус в шкале F является редуктом шкалы G.
    Проблема «по двум конечным шкалам G и F выяснить, верно ли включение Logic(G) ⊆ Logic(F)» алгоритмически разрешима.
    Логика меньшего конуса не может содержаться в логике большего конуса: если Logic(G) ⊆ Logic(F), то |G|≥|F|.
    Если логика одного конечного конуса G строго содержится в логике другого конечного конуса F, то первый конус строго больше второго: |G|>|F|.

  6. 2020.04.10: Характеристическая формула глубины d конечного конуса.
    Два способа ее построения: а) с использованием переменных по точкам; б) с использованием переменных по подмножествам. Доказательство взаимной выводимости множеств формул, описывающих шкалу двумя разными способами. (В случае логики K4 это будет означать дедуктивную эквивалентность двух видов характеристических формул.)

    Характеристическая формула конечного транзитивного конуса. Теорема о характеристической формулы (уже без d). Ее переформулировка в форме теоремы о расщеплении полных логик. Характеристическая формула (конечного транзитивного конуса) является дедуктивно наислабейшей формулой (над K4). Переформулировка этой теоремы в форме расщепления для конечно аксиоматизируемых логик. Теорема о расщеплении для всех (нормальных) логик, содержащих K4.
    Таким образом, всякий конечный транзитивный конус (а значит, и всякая конечная транзитивная шкала, будучи пересечением логик своих конусов?) расщепляет решетку нормальных расширений K4.

    Теорема Блока — критерий того, что конечная шкала расщепляет решетку всех нормальных логик (без доказательства).


  7. 2020.04.17:

  8. 2020.04.24:

  9. 2020.05.08:

  10. 2020.05.22: