О модальных логиках элементарных классов шкал Крипке

• Автор: Кикоть, Станислав Павлович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2010
• Место защиты: Москва
• Количество страниц: 122 с. : ил.

Оглавление
Введение

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

1 Предварительные сведения из модальной логики

1.1 Синтаксис

1.2 Семантика Крипке

1.3 Конструкции, сохраняющие истинность

1.4 Обобщенные шкалы

1.5 Теоремы Салквиста и Крахта

2 Обобщенные формулы Салквиста

2.1 Регулярные П-формулы

2.2 Безопасные термы
2.3 Обобщенные формулы Салквиста
2.4 й-упорство
2.5 Обобщенные формулы Крахта
2.5.1 Определения и примеры
2.5.2 Квази-безопасные выражения
2.5.3 Доказательство обобщенной теоремы Крахта
2.6 Неэквивалентность обобщенных формул Крахта стандартным
3 Формулы, соответствующие диаграммам
3.1 Постановка задачи
3.2 Экзистенциальные диаграммы
3.3 Неопределимые экзистенциальные диаграммы
3.4 Определимые экзистенциальные диаграммы
3.5 Достаточное условие модальной определимости для УЗ-диаграмм
4 Двумерные модальные логики с выделенной диагональю.
4.1 Формулировка теоремы
4.2 Доказательство основной теоремы
Приложение 1. Критерий модальной определимости для УЗ-диаграмм

ВВЕДЕНИЕ

Актуальность темы
Модальная логика изучает модальные операторы — математические модели языковых конструкций, которые действуют как одноместные пропозициональные связки.
Сюда относятся самые разнообразные операторы, касающиеся необходимости и возможности (“необходимо, что” и “возможно, что”), доказуемости (“доказуемо, что...”), знания (“Агент А знает, что...”), веры (“Агент А верит, что...”), пространства (“везде”, “где-то”, “в некоторой окрестности”, “в Москве”), времени (“всегда”, “всегда в будущем”, “завтра”), и др. Модальная логика тесно связана с логикой первого по-

рядка, а именно, классические кванторы /х и Зх тоже можно считать модальными операторами. В настоящее время модальная логика активно развивается, благодаря разнообразным применениям — в том числе в информатике, математической лингвистике и основаниях математики.
Начиная с конца 1950-х годов в модальной логике получила широкое распространение реляционная семантика Крипке [26]. Основная ее идея заключается в том, что формулы интерпретируются в реляционных структурах (“шкалах Крипке”), а формула аф считается истинной в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению.
На основе семантики Крипке были вскоре построены адекватные семантики для большого числа модальных исчислений, и была разработана соответствующая теоретико-модельная техника. Появились и общие результаты о семантике модальных логик, такие как теорема Салквиста [30] или Гольдблатта-Томасона [10]. Появились и отрицательные результаты: примеры неполных по Крипке модальных исчислений, исчислений с алгоритмически неразрешимой проблемой вывода.

Одним из трудных нерешенных вопросов в теории модальных логик остается вопрос о том, каким образом комбинировать логики с разнородными модальными операторами. Одна из трудностей заключается в том, что эти модальные операторы могут “взаимодействовать”. Простейший пример такого взаимодействия представляют собой коммутирующие операторы, такие как “всегда” и “везде” (формулы “везде всегда Л” и “всегда везде А” разумно считать равносильными, если объем понятия “везде” не меняется со временем).
Для работы с такого рода операторами в 1970ее гг было предложено интепре-тировать формулы в прямых произведениях реляционных структур, что послужило началом “многомерной модальной логики”. Сейчас это активно развивающийся раздел модальной логики; систематическое изложение теории произведений содержится в книге [7]. Также отметим, что конструкции, похожие на произведения (предикатные шкалы Кринке с постоянной областью), возникают при изучении модальных и интуиционистских логик предикатов [9].
Основные задачи этой области традиционны для математической логики: установить аксиоматику для заданного класса структур-произведений, исследовать разрешимость и сложность получающихся логик.
Нетрудно установить [8], что прямое произведение элементарных классов элементарно. Поэтому изучение произведений тесно связано с исследованием произвольных элементарных классов шкал Кринке, которому посвящена настоящая диссертация.
Однако модальные логики элементарных классов до сих пор были изучены недостаточно глубоко.
Из положительных результатов отметим теорему Салквиста ([30]; современное изложение см. в [2],[4]), описывающую большой класс элементарных канонических модальных формул, и теорему Крахта ([24], [25]), описывающую их классические первопорядковые эквиваленты.
Большинство современных доказательств теорем о полноте для различных модальных логик опираются на теорему Салквиста. В связи с этим существенным продвижением является обобщение теоремы Салквиста ([11], [12], [21]), которому посвящена глава 2 этой диссертации, так как оно существенно расширяет класс известных

• формула (Зх1>£ Су)ф истинна в том и только том случае, когда найдется такая точка ш 6 IV, что уЩ^ш, и в модели М истинна формула ф[сш/х.
Формула Л языка ТС/= называется чистой, если РУ(Л) П ВУ(А) = 0 и разные кванторы связывают разные переменные.
Формула языка 7£/= называется позитивной, если она не содержит связок -> и —+.
ОПРЕДЕЛЕНИЕ 1.58. Назовем переменную х в чистой формуле ф квази-свободной, если либо х свободна, либо х связана (ограниченным) квантором всеобщности, который не находится внутри области действия никакого квантора существования.
Формула А языка 7£/3 называется формулой Крахта, если А
• содерл^ит ровно одну свободную переменную,
• чиста,
• позитивна (то есть не содержит -1 и —>),
• в каждой подформуле вида хНАу по крайней мере одна из переменных х и у квази-свободна.
ТЕОРЕМА 1.59 (Теорема Крахта, [24], [25]).
• Любая формула Крахта ф является нервопорядковым эквивалентом некоторой формулы Салквиста.
• Любая формула Салквиста ф является модальным эквивалентом некоторой формулы Крахта.