О модальных логиках элементарных классов шкал Крипке тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Кикоть, Станислав Павлович

• Кикоть, Станислав Павлович
• кандидат физико-математических наук
• 2010

Оглавление диссертации кандидат физико-математических наук Кикоть, Станислав Павлович

Введение

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

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

1.1 Синтаксис.

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

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

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

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

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

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

2.2 Безопасные термы.

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

2.4 d-упорство

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 Доказательство основной теоремы.

Введение диссертации (часть автореферата) на тему «О модальных логиках элементарных классов шкал Крипке»

Актуальность темы

Модальная логика изучает модальные операторы — математические модели языковых конструкций, которые действуют как одноместные пропозициональные связки.

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

Начиная с конца 1950-х годов в модальной логике получила широкое распространение реляционная семантика Крипке [26]. Основная ее идея заключается в том, что формулы интерпретируются в реляционных структурах ("шкалах Крипке"), а формула □ ф считается истинной в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению.

На основе семантики Крипке были вскоре построены адекватные семантики для большого числа модальных исчислений, и была разработана соответствующая теоретико-модельная техника. Появились и общие результаты о семантике модальных логик, такие как теорема Салквиста [30] или Гольдблатта-Томасона [10]. Появились и отрицательные результаты: примеры неполных по Крипке модальных исчислений, исчислений с алгоритмически неразрешимой проблемой вывода.

Одним из трудных нерешенных вопросов в теории модальных логик остается вопрос о том, каким образом комбинировать логики с разнородными модальными операторами. Одна из трудностей заключается в том, что эти модальные операторы могут "взаимодействовать". Простейший пример такого взаимодействия представляют собой коммутирующие операторы, такие как "всегда" и "везде" (формулы "везде всегда Л" и "всегда везде А" разумно считать равносильными, если объем понятия "везде" не меняется со временем).

Для работы с такого рода операторами в 1970ее гг было предложено интепре-тировать формулы в прямых произведениях реляционных структур, что послужило началом "многомерной модальной логики". Сейчас это активно развивающийся раздел модальной логики; систематическое изложение теории произведений содержится в книге [7]. Также отметим, что конструкции, похожие на произведения (предикатные шкалы Кринке с постоянной областью), возникают при изучении модальных и интуиционистских логик предикатов [9].

Основные задачи этой области традиционны для математической логики: установить аксиоматику для заданного класса структур-произведений, исследовать разрешимость и сложность получающихся логик.

Нетрудно установить [8], что прямое произведение элементарных классов элементарно. Поэтому изучение произведений тесно связано с исследованием произвольных элементарных классов шкал Крипке, которому посвящена настоящая диссертация.

Однако модальные логики элементарных классов до сих пор были изучены недостаточно глубоко.

Из положительных результатов отметим теорему Салквиста ([30]; современное изложение см. в [2],[4]), описывающую большой класс элементарных канонических модальных формул, и теорему Крахта ([24], [25]), описывающую их классические первопорядковые эквиваленты.

Большинство современных доказательств теорем о полноте для различных модальных логик опираются на теорему Салквиста. В связи с этим существенным продвижением является обобщение теоремы Салквиста ([11], [12], [21]), которому посвящена глава 2 этой диссертации, так как оно существенно расширяет класс известных элементарных модальных формул и полных модальных логик. В работах [34], [35] класс элементарных модальных формул синтаксически был расширен еще сильнее, но первопорядковые аналоги новых формул оказались эквивалентны старым. Ведутся работы по компьютерному поиску элементарных модальных формул [5], [6].

Можно еще отметить недавнюю работу [15], приводящую явную бесконечную модальную аксиоматику для любого элементарного класса, а также работу [1], в которой показано, как существенно упростить эту аксиоматику для ряда особых случаев.

Однако, поиски общих результатов о модальных логиках элементарных классов шкал, (например, критерия конечной аксиоматизируемости), принципиально ограничены неразрешимостью классической логики первого порядка. Общие проблемы "по первопорядковой формуле определить, является ли она модально определимой", и "по модальной формуле определить, является ли она элементарной" алгоритмически неразрешимы [3].

Тем не менее, в главе 3 диссертации получены наглядные необходимые и достаточные условия модальной определимости для некоторых формул первого порядка, а именно, для формул, которые можно описать при помощи графов специального вида, называемых диаграммами.

В [37] модальная определимость формул первого порядка используется для конструирования алгоритмов, отвечающих на запросы к базам данных. Также в этой работе доказан частный случай Теоремы 3.16 для случая одной единственной черной точки. Интересно, что в этом доказательстве использовались операции на графах, аналогичные последовательному и параллельному соединению проводников.

В главе 4 изучается общая конструкция ¿-квадрата произвольной 1-модальной логики Ь. Именно, ¿-квадратом 1-шкалы Кригхке Р — К) называется шкала {XV х И7, 74, Нь,. А), где Я^, Я^ — стандартные вертикальные и горизонтальные отношения, а диагональ Д = {(а, а) | а £ И^}. ¿-квадратом 1-модальной логики Ь называется множество формул в языке с модальностями 0/(, и пропозициональной константой ¿, общезначимые на ¿-квадратах всех шкал многообразия логики Ь (6 верна в точности в точках диагонали).

Эта конструкция обобщает обычное произведение модальных логик по аналогии с давно известным построение логики 5-квадратов шкал Крипке с унивесальным отношением Бб^,, связанной с цилиндрическими алгебрами.

Напомним, что представимой цилиндрической алгеброй размерности п над множеством IV называется множество всех подмножеств с операциями цилиндри-фикации

Зг(т4) = {Ь | Ь =г а для некоторого а & А}, где запись Ь а означает, что кортежи Ь и а совпадают на всех своих элементах, кроме, быть может, г-ого, и выделенными элементами

4,- = {а | (11 = а^}, где щ и а^ обозначают г-ый и ^'-ый элементы кортежа. Элементы могут отсутствовать; в этом случае говорят о бездиагональных цилиндрических алгебрах.

Это понятие было введено Тарским в конце сороковых для алгебраической интерпретации логики предикатов, и представляет собой один из основных объектов исследования алгебраической логики. Цилиндрические алгебры тесно связаны с многомерными медальными логиками: например, многообразие бездиагональных пред-ставимых цилиндрических алгебр размерности п совпадает с многообразием модальных алгебр логики Эб™.

Легко видеть, что модальная алгебра декартова квадрата шкалы Р = (\¥,1Ух \¥) с отмеченной диагональю является представимой цилиндрической алгеброй размерности 2. Поэтому логика Бб^ [29] соответствует универсальному фрагменту теории представимых цилиндрических алгебр размерности 2. Используя аксиоматику для этой цилиндрической алгебры из [14], Иде Винема в [36] построил конечную аксиоматику для логик Бб^, и 85^.

Как оказалось, конечная аксиоматика для Бб^, является скорее исключением, чем правилом для квадратов. Основной результат главы 4 этой диссертации заключается в том, что, в отличие от обычных произведений, которые часто обладают конечной аксиоматикой ([38], см. также теорему 5.9 на стр. 230 в [7]), для любой модальной логики Ь, такой что К С Ь С Сгг или КС1С СЬ, ее 5-квадрат не аксиоматизируем при помощи конечного количества переменных. Используемый метод доказательства восходит к работе [16].

Весьма трудны и интересны алгоритмические вопросы, связанные с ¿-квадратами. Недавно было показано [29], что многие ¿-квадраты (среди которых логика не финитно аппроксимируемы. В самое последнее время автором совместно с А. Куруш была установлена неразрешимость логики но вопрос о разрешимости логик и Т^ пока открыт.

Цель работы

Целью данной работы является изучение модальных логик различных элементарных классов шкал Крипке.

Научная новизна

Основные результаты диссертации являются новыми и состоят в следующем:

1) Получено новое доказательство обобщенной теоремы Салквиста, первоначально опубликованной в работах [11] и [12]. Это доказательство получено независимо, не использует многоместных модальностей и, в отличие от доказательства В. Горанко и Д. Вакарелова, дает явные формулы для минимальной оценки.

2) Получено явное синтаксическое описание формул первого порядка, которые являются переводами обобщенных формул Салквиста.

3) Построен новый пример обобщенной формулы Салквиста, которая не эквивалентна никакой стандартной формуле Салквиста.

4) Получен критерий модальной определимости для экзистенциальных формул первого порядка, бескванторная часть которых представляет собой конъюнкцию атомарных. Критерий заключается в отсутствии в графе, соответствующем формуле, циклов специального вида. Для определимых формул предъявлен алгоритм построения определяющего вектора модальных формул.

5) Получено достаточное условие модальной определимости для некоторого класса универсально-экзистенциальных формул первого порядка, описываемых при помощи специальных графов.

6) Показано, что логики квадратов шкал Крипке с выделенной диагональю, как правило, не аксиоматизируются при помощи формул с фиксированным конечным множеством переменных. Методы исследования

Обобщенная теорема Салквиста доказывается аналогично стандартной, с использованием метода ван Бентема подстановки минимальных оценок [2] и топологических свойств канонической шкалы [31], [32].

Для доказательства неэквивалентности обобщенных формул Крахта стандартным формулам Крахта используются теоретико-модельные игры.

Для доказательства модальной неопределимости диаграмных формул с циклом используется инвариантность модальных формул относительно ультрарасширений.

Для доказательства модальной определимости диаграмных формул без циклов используется обобщение теоремы Крахта, полученное в главе 2.

Для доказательства конечной неаксиоматизируемости логик квадратов шкал Крипкс с выделенной диагональю в главе 4 используются обобщенные формулы Салквиста, которые строятся при помощи алгоритма, изложенного в главе 3.

Теоретическая и практическая ценность

Работа носит теоретический характер. Полученные в ней результаты могут быть полезны специалистам, работающим в МГУ им. М. В. Ломоносова, Математическом институте РАН им. В. А. Стеклова, Тверском государственном университете, Петербургском отделении математического института РАН им. В. А. Стеклова, Институте математики им. С. Л. Соболева СО РАН, Институте проблем передачи информации РАН им. А. А. Харкевича.

Апробация работы I

Результаты диссертации докладывались в 2003-2010 гг.:

• на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов механико-математического факультета МГУ под руководством академика РАН С.И. Адяна, член-корр. РАН Л.Д. Беклемишева и проф. В.А. Успенского, и других семинарах кафедры;

• на Международной конференции «Алгебраические и топологические методы в неклассических логиках II» (Барселона, Испания, 2005);

• на Международной конференции «Приложения модальной логики в информатике» (Москва, 2005);

• на Международной конференции «Advances in Modal Logic, 2008» (Нанси, Франция, 2008),

• на XXXI конференции молодых ученых (МГУ, 2009); Публикации

Результаты автора по теме диссертации опубликованы в 7 работах: [21], [20], [22], [18], [19], [23], [17]. Из них одна работа ([18]) опубликована в журнале из "Перечня ведущих рецензируемых научных журналов и изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученой степени доктора и кандидата наук".

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

В первой главе содержатся основные сведения, определения и результаты из модальной логики. Приведем те из них, которые необходимы для точной формулировки результатов диссертации.

Фиксируем счетное множество пропозициональных переменных PV и некоторое множество индексов Е.

ОПРЕДЕЛЕНИЕ (1.1). Формулы языка Mis (модальные формулы) строятся рекурсивно с помощью переменных из PV, констант «ложь» (L), «истина» (Т), логических связок A, V, —>, -1 и двойственных друг к другу модальностей df и О^ для каждого £ G S.

ОПРЕДЕЛЕНИЕ (1.55). Формула называется позитивной, если она не содержит связок -1 и —» (но может содержать !). Формула называется негативной, если она есть отрицание позитивной.

ОПРЕДЕЛЕНИЕ (1.4). Шкалой Кринке для языка называется набор F =

IV, (Rç : £ G H)), где Rç С W х W для каждого £ G Е. Элементы множества W мы будем называть точками.

ОПРЕДЕЛЕНИЕ (1.5). Оценкой в шкале Кринке F = (W, (Rç : £ G E)) называется отображение в : PV —» 2W, которое каждой пропозициональной переменной ставит в соответствие множество точек шкалы Крипке.

ОПРЕДЕЛЕНИЕ (1.6). Моделью Крипке, построенной на шкале F, называется пара M — (F, 9), где 0 — оценка в шкале F.

ОПРЕДЕЛЕНИЕ (1.7). Истинность формулы в точке модели M = (F, в) определяется стандартным образом:

• в точке х переменная р G PV истинна, если х G в(р);

• значения булевых связок вычисляются в точке по классическим таблицам истинности;

• в точке х истинна формула О^ф, если найдется такая точка у £ в которой верна формула ф\

Запись F, w, в \= ф означает, что формула ф истинна в точке w модели М = (F, в). определение (1.14). Запись F, w f= ф означает, что формула ф истинна в точке w любой модели М, построенной на шкале F. определение (1.15). Формула ф общезначима на шкале F, если она истинна во всех точках любой модели М, построенной на шкале F.

Шкалу Крипке F = (W, (Я^ : £ € Е)) можно рассматривать как обычную модель для языка первого порядка С,содержащего равенство, бинарные предикатные символы В$ для каждого £ е Е, предметные переменные и кванторы. определение (1.18). Первопорядковая формула А{х) языка £/= с одной свободной переменной х соответствует модальной формуле ф языка М.1-=, если в любой шкале Крипке F для любой ее точки w

F, w (= ф в шкале F верна формула A(w). определение (1.19). Первопорядковая формула А(х) языка £/н с одной свободной переменной х называется модально определимой, если она соответствует некоторой модальной формуле ф. определение (1.22). Первопорядковая формула А(х\,., хп) языка £/ со свободными переменными ., хп называется модально определимой, если существует такая последовательность модальных формул ф\,., фп, что в любой шкале Крипке F для любых ее точек wi,. ,wn для любой оценки в для некоторого г (1 < г < n) F, wt, в [= фг <£=>■ в шкале F верна формула A[w\,., wn]. определение (1.20). Модальная формула называется (локально) элементарной, если она соответствует некоторой формуле первого порядка языка Cf3.

ОПРЕДЕЛЕНИЕ (1.38). Обобщенной шкалой Крипке для языка М.1^ называется набор ^ - (\¥, : ( е Е), А), где Щ С V/ х IV для всех ^ £ Б, А С 2Ц/, и А замкнуто относительно булевых операций и операции У —»

ОПРЕДЕЛЕНИЕ (1.39). Пусть ^ = (1У, (Я^ : £ £ 5), Л) — обобщенная шкала Крипке. Оценка в : РУ —> 2У/ называется допустимой для если она принимает значения в А.

Истинность формулы в обобщенной шкале определяется так же, как и в шкале Крипке.

ОПРЕДЕЛЕНИЕ (1-41). Модальная формула общезначима в обобщенной шкале Р, если она верна во всех точках шкалы при любой допустимой для Р оценке.

Положим для V С Ж /?°(У) = {х | ^(х) С V}. ОПРЕДЕЛЕНИЕ (1.42). Обобщенная шкала Крипке Р = называется

• различимой, если для любых различны х, у из IV найдется такое У £ А, что х £ V и у <£У.

• тугой, если

П^ е л I ЯеИ ^ £

• компактной, если любое центрированное семейство (т. е. семейство, пересечение любого конечного множества элементов которого не пусто) Ы С А имеет непустое пересечение.

• дескриптинной, если Р различима, туга и компактна.

ОПРЕДЕЛЕНИЕ (1.43). Модальная формула ф называется (1-упорной, если для любой дескриптивной обобщенной шкалы Р = (\У, {Щ : £ € Н),.А) из общезначимости ф на Р, следует ее общезначимость и на соответствующей обычной шкале Крипке

Вторая глава посвящена обобщенным формулам Салквиста и их первопорядко-вым аналогам — обобщенным формулам Крахта.

Будем считать, что множество переменных РУ разбито на счетное множество групп р°, Рз) Рз) • • •> р\) Рз> • • ■> Р\ > р!) Vз,. и т. д. Верхний индекс (называемый рангом) означает номер группы, а нижний — номер переменной в пределах группы.

ОПРЕДЕЛЕНИЕ (2.2). Регулярная П-формуларанга к определяется по индукции. Именно,

• любая переменная $ ранга к является П-формулой ранга к,

• если РОБ — позитивная модальная формула, зависящая только от переменных, ранг которых меньше к и ф — регулярная П-формула ранга к, то РОБ —> ф — регулярная п-формула ранга к.

• если ф —регулярная П-формула ранга к, то — тоже регулярная П-формула ранга к.

ОПРЕДЕЛЕНИЕ (2.29). Обобщенной импликацией Салквиста называется формула вида СБА —> ±, где СБА построена из регулярных П-формул и негативных формул при помощи А, V, О^.

ОПРЕДЕЛЕНИЕ (2.30). Обобщенной формулой Салквиста называется модальная формула, построенная из обобщенных импликаций Салквиста при помощи А, П^, а так же V, применяемой к формулам без общих пропозициональных переменных.

ТЕОРЕМА (2.32, Обобщенная теорема Салквиста). Каждая обобщенная формула Салквиста элементарна и ¿-упорна.

ОПРЕДЕЛЕНИЕ. Модальная логика А называется полной, если любая совместная с пей формула (т. е. такая формула ф, что ф —» 1 ^ А) выполнима на некоторой шкале Крипке, на которой А общезначима.

СЛЕДСТВИЕ. Логика, аксиоматизируемая обобщенными формулами Салквиста, полна.

ОПРЕДЕЛЕНИЕ. Ь-термом называется терм в языке, алфавит которого состоит из символов {:Ег}, П, и, Я^1, Я°, Щ, Т, !. Здесь 1, Т — константы, {х{} — переменные, Я"1, Я°, Я$ — одноместные функциональные символы, П, и — бинарные функциональные символы.

ОПРЕДЕЛЕНИЕ (2.19). Назовем Ь-терм ,ч полубезопасным, если верно одно из следующих условий:

1) з = {а*};

2) в — Я^(й'), где з' полубезопасен;

1)

2)

3) 4)

5)

6)

Рис. 1: Примеры диаграмм ТЕОРЕМА (2.52, Обобщенная теорема Крахта).

• Каждая обобщенная формула Салквиста соответствует некоторой обобщенной формуле Крахта.

• Каждая обобщенная формула Крахта соответствует некоторой обобщенной формуле Салквиста.

Естественный вопрос: а будет ли семантически класс обобщенных формул Крахта шире класса стандартных формул Крахта? Ответ на этот вопрос дает следующая

ТЕОРЕМА (2.66). Обобщенная формула Крахта с = Ух1 >1 хУх2 >2 1>з хЗу' >1 хЗу" >2 у'Зу >3 у" у <= Я3(Я2(Х1) П Яг(х2)) Л у е Я2(Яз(х!) П ЯгЫ) А А у е Яг(Я2(хг) П Я3{х2)) ), выражающее "свойство куба" трехмерного произведения шкал Крипке, не эквивалентна никакой стандартной формуле Крахта.

Третья глава посвящена формулам первого порядка с одной свободной переменной, которые можно проиллюстрировать специальным чертежом — диаграммой.

На Рис. 1 приведены простейшие примеры таких диаграмм: (условия станут более привычными,, если их мысленно дополнить квантором всеобщности по х)

1) транзитивность: УуУг(хЯу А уЯг —>• хЯл).

2) плотность: Уг{хЯг —> 3у(хЯу А уЯг)).

3) полукоммутативность: \/у(хЯ2Ягу хЯ.\ Я2у).

4) свойство Черча-Россера: ЧуУг(хЯгу А хЯ2г —> Зу(уЯ^ А гЯ\ю)).

3) 5 = в' П в", где либо з', либо в" полубезопасен.

Терм £ называется безопасным, если он полу безопасен, и в каждом его подтерме вида Щ(з) терм й нолубезопасен.

ОПРЕДЕЛЕНИЕ. Ограниченными кванторами называются конструкции х^) и (зхг >? ху), где

Ухг := \/Xi(xjЩxi —»■ а);

За^ Ху)а := Зх{(х3-Я(хг А а).

Рассмотрим язык первого порядка 7^/н, содержащий предметные переменные а^, логические связки А и V, ограниченные кванторы и по (п-Ы)-местному предикатному символу \у £ Е для каждого безопасного терма Е, содержащего п различных х^.

Ясно, что любую такую формулу можно перевести на классический язык первого порядка, заменив предикатный символ у £ Е на его перевод Е*(ь), где ж* }*(» := (и = Хг);

Т» := Т;

Ег и Е2)*{у) := Е{{у) V Е*(у);

Щ\Е)У(у) := Зу(уВ,£у Л Е*(у)[у/у])-,

Е)Г(у) := Му{уЩу Я*(т;)[у/1;]);

Яс(£))>) := А Е*(у)[у/у}).

В последних трех случаях у должна быть некоторой новой переменной, не встречающейся в формуле Е*{у).

ОПРЕДЕЛЕНИЕ (2.49, 2.50). Формула А(х0) в этом языке называется обобщенной формулой Крахта, если она содержит ровно одну свободную переменную Хо и построена из формул вида у £ Е при помощи конъюнкции, дизъюнкции и ограниченных кванторов, причем для каждой подформулы вида у £ Е , входящей в А(хо), все переменные хг, входящие в Е, квази-свободны, то есть связаны ограниченным квантором всеобщности, который не находится под действием никакого ограниченного квантора существования.

5) сериальность: 3у хЯу.

6) симметричность: Уу(хЯу —>■ уЯх).

Сперва мы рассматриваем так называемые экзистенциальные диаграммы, которые получаются из приведенных рисунков удалением сплошных стрелок.

ОПРЕДЕЛЕНИЕ (3.1). Экзистенциальной диаграммой называется набор С = {У/, \¥Ч,\¥В)Т11,.) ПД где\¥ = \¥чи\УБ,\¥чП\Ув = $иТ1гС\¥х УУ.

Положим \¥ч = ., хп}, \УВ = (т/1,., Ут}. Точки множества будем называть черными, а точки множества \УВ — белыми. Каждой тот1ке г Е Ш поставим в соответствие предметную переменную уг.

Каждой экзистенциальной диаграмме С поставим в соответствие формулу Кс в языке первого порядка с з бинарными предикатами Я],., Я3 и п + т свободными переменными уХ1,., ьХл, иУ1,., иУт

-с

А Д и формулу

Ес в том же языке первого порядка с п свободными переменными

Ес = Зуш.ЗуутКс.

ОПРЕДЕЛЕНИЕ. Экзистенциальная диаграмма С называется определимой, если первопорядковая формула Ес(иХ1,. ,уХп) модально определима.

Наша цель — получить критерий определимости для диаграмм.

ОПРЕДЕЛЕНИЕ (3.7). Пусть ., ьп) и В{ьъ .,уп)— две формулы языка £/ с одними и теми же свободными переменными. Мы говорим, что из формулы А следует формула В (обозначаем А \= В), если в любой модели Р = (И7, Яг,., Я3) для любого набора точек ., € из того, что Р \= А(г>°,. г>°) следует, что

ОПРЕДЕЛЕНИЕ (3.8). Экзистенциальная диаграмма С называется минимальной, если для любой диаграммы С, которая получается из диаграммы С удалением какой-нибудь стрелки, из формулы Ес' не следует формула Ес.

Говоря неформально, минимальность диаграммы означает, что все ее ребра "существенны", то есть никакое ребро нельзя выкинуть без потери семантического смысла диаграммы.

ОПРЕДЕЛЕНИЕ. Направленным путем в экзистенциальной диаграмме С, соединяющим точку х с точкой у, называется такая последовательность ос^а^ . £/га;/1+1, где для всех г от 1 до /г. а* е IV, & £ {1,., в} и (а*, аг+1) е П^, и, к тому же, а.\ = х и ан = у.

Ненаправленный путь отличается от направленного тем, что условие {щ, £ П^ заменяется на (о^о^!) £ П^ иП^1.

ОПРЕДЕЛЕНИЕ (3.5). Экзистенциальная диаграмма называется достижимой, если для любой белой точки у найдется черная точка х, такая что существует направленный путь, соединяющий точки х и у, все точки которого, кроме х, белые.

ОПРЕДЕЛЕНИЕ (3.11). Экзистенциальная диаграмма называется связной, если любые две белые точки можно соединить ненаправленным путем, все точки которого белые.

ОПРЕДЕЛЕНИЕ (3.13). Пусть С = {XV, П1;., Пв) - экзистенциальная диаграмма. Мы говорим, что она содержит петлю, если для некоторых х е и £ € {1,.,з} (х, х) е П^. Мы говорим, что она содержит кратное ребро, если для некоторых £ {!,•■•, ¿'Ь £1 Ф £2 х И^) ПП^ ПП^2 ф 0, или же для некоторых, возможно равных, £1,^2 £ {1,.,з}, найдутся точки х,у 6 такие что хИ^у и уП.£2х. Мы говорим, что диаграмма содержит внутренний цикл, если она либо содержит петлю, либо кратное ребро, либо ненаправленный путь а^а^г ■ • • Ь^н+х (к > 3), где все щ е И^, у которого все вершины белые, и все вершины которого, кроме первой и последней, попарно различны, а первая и последняя совпадают.

ТЕОРЕМА (3.15). Если достижимая минимальная экзистенциальная диаграмма содержит внутренний цикл, то она модально неопределима.

ТЕОРЕМА (3.16). Если достижимая связная экзистенциальная диаграмма не содержит внутренних циклов, то она модально определима.

СЛЕДСТВИЕ (Критерий определимости). Достижимая связная минимальная диаграмма модально определима тогда и только тогда, когда она не содержит внутренних циклов.

СЛЕДСТВИЕ (3.17). Если достижимая экзистенциальная диаграмма С не содержит внутренних циклов, то задаваемая ей первопорядковая формула Е°(уХ1,., иХп ) представляет собой конъюнкцию определимых первопорядковых формул.

Затем мы переходим к изучению диаграмм со сплошными стрелками.

ОПРЕДЕЛЕНИЕ. 2.33 Пусть дан набор Т = (Ж, ., Дв), где все Щ С IV х IV. Два направленных пути х^, £1, х2, • • ■ хп и у\, //1, У2, /¿2, ■ ■ ■ ут мы считаем равными, если т = п, Хг = у1 для всех 1<г<пи& = /х* для всех 1 < г < п — 1. Набор Т = (Т, г) называется деревом с корнем г, если

• г е IV,

• Щг(г) = 0 для всех ^еН,

• для любой точки х, отличной от корня, существует единственный путь, соединяющий тех.

ОПРЕДЕЛЕНИЕ (3.29). УЗ-диаграммой будем называть набор О = (IV, Вг,., В3, П1;., П3, г), где ]¥ — конечное множество, IV = У/ч и \¥в, ч П = 0, £?!,., Д, — бинарные отношения на \¥ч, П1,.,П5 — бинарные отношения на \¥ и г £ \УЧ, причем структура (1УЧ, В\,. ,В5,г) представляет собой дерево с корнем г. Элементы множеств Bj и П^ будем называть соответственно черными и белыми стрелками.

ОПРЕДЕЛЕНИЕ (3.30). Экзистенциальной частью УЗ-диаграммы В ~ \¥ч, \¥в, В\,., В8, Пх,., П8, г) будем называть экзистенциальную диаграмму С={Ш,\¥Ч,\УЪ, ПЬ.,П3).

Как и для экзистенциальных диаграмм, положим \¥ч = {хо,Х1,. ,хп}, ]¥в = {у\,., угп}, причем будем считать, что х0 = г, и каждой точке 2: £ IV поставим в соответствие предметную переменную

Каждой УЗ-диаграмме Б поставим в соответствие первопорядковую формулу Е0 с одной свободной переменной ьхо в сигнатуре с я бинарными предикатными символами Д1,., Я.а:

ОПРЕДЕЛЕНИЕ (3.32). УЗ-диаграмма £> = (Ш, \¥ч, 1УГ„ Въ ., Ва, Пь ., Па,г) называется минимальной (достижимой, содержащей внутренний цикл), если ее экзистенциальная часть обладает соответствующим свойством.

ОПРЕДЕЛЕНИЕ (3.31). УЗ-диаграмма И = Вг,., Ва, Пг,., Пя, г) называется модально определимой, если формула Ер модально определима.

ТЕОРЕМА (3.33). Если достижимая УЗ-диаграмма О не содержит внутренних циклов, то она модально определима.

В Приложении 1 мы приводим критерий модальной определимости для некоторого класса УЗ-диаграмм.

В четвертой главе методы, разработанные в главах 2 и 3, применяются к модальным логикам квадратов шкал Крипке с выделенной диагональю. Основной результат главы — неаксиоматизируемость большого числа таких логик при помощи формул с конечным числом переменных.

Для работы с двумерными произведениями с выделенной диагональю используется язык Его алфавит получается из бимодального языка Л41{ь,у} добавлением пропозициональной константы 3.

Шкалой Крипке (для языка Л41$) будем называть набор Е = (У/, Лу, Д), где И^ С IV х № (£ Е {/>,, г?}), Д С IV. Моделью Крипке называется пара М = (/% в), где Р — шкала Крипке, а в — оценка в шкале Е.

Определение истинности формулы в модели Крипке получается из стандартного определения добавлением пункта

• формула 8 истинна в точности в точках множества Д. где а С — экзистенциальная часть П.

На этот язык очевидным образом переносится понятие общезначимости формулы и модальной логики класса шкал.

ОПРЕДЕЛЕНИЕ (4.6). Множество формул Е аксиоматизирует логику L, если L является минимальным множеством формул, содержащим все пропозициональные тавтологии, формулы Kh, Kv, где

К£ = □ g(p q) -> (П5р ->• D^), множество формул Е, и замкнутое относительно правил вывода Modus Ponens, правила подстановки и правила обобщения:

А,А^В А А

В, [В/р]А, DiA.

ОПРЕДЕЛЕНИЕ (4.7). Логика L аксиоматизируема формулами с конечным числом переменных, если существует такое множество модальных формул Е, что оно аксиоматизирует логику L, и в формулы Е входит лишь конечное число переменных.

ОПРЕДЕЛЕНИЕ (4.1). Пусть F = (W, R) - 1-шкала Кринке. Через F| обозначим шкалу (W х W, Rh, Ry, А), где а, b)Rh(c, d) -Ф=Ф- aR,c и b = d\ а, Ь)Л„(с, d) а — с и bRd, А = {(а, а) | а е W}. Такую шкалу мы будем называть 5-квадратом шкалы F.

ОПРЕДЕЛЕНИЕ (4.2). Пусть С — класс 1-шкал Крипке. Положим

Cf = № \FtC}.

ОПРЕДЕЛЕНИЕ (4.4). Пусть L — полная по Крипке 1-модальная логика. 5-квадратом логики L (обозначается Щ) называется множество формул Log (C(ij)f), где C(L) — класс всех 1-шкал Крипке, на которых общезначима логика L.

Чтобы точно сформулировать результат о неаксиоматизируемости формулами с конечным числом переменных, рассмотрим следующие шкалы Крипке (см. Рис. 2). щ Щ

Рис. 2: Шкалы Щ и

Формально, = Н„), где {0,1,., п, 1,., гг, с},

К = {(М I 1 < г < га} и {(г, Л I 1 < ^ 7 < га} и {(г, с) | 1 < г < гг}, = где = {г, 1,. .п}, ^ = {(г,г) | 1 < г < гг}.

ТЕОРЕМА (4.9). Пусть Ь — полная по Крипке 1-модальная логика, и С(Ь) содержит все шкалы вида И''] и Отп или все их рефлексивные замыкания, или все их транзитивные замыкания, или все их рефлексивные транзитивные замыкания. Тогда не аксиоматизируема формулами с конечным числом переменных.

СЛЕДСТВИЕ (4.10). Дельта-квадраты любой полной по Крипке логики Ь, такой что К С Ь С СЬ или К С Ь С вгг, не аксиоматизируемы формулами с конечным числом переменных.

Список литературы диссертационного исследования кандидат физико-математических наук Кикоть, Станислав Павлович, 2010 год

1. P. Balbiani, 1. Shapirovsky, and V. Shehtman. Every world can see a Sahlqvist world. In Governatori et al. 13], pages 69-85.

2. P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2002.

3. A. Chagrov and L. Chagrova. The truth about algorithmic problems in correspondence theory. In Governatori et al. 13], pages 121-138.

4. A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press, 1997.

5. W. Conradie, V. Goranko, and D. Vakarelov. Algorithmic correspondence and completeness in modal logic. The core algorithm SQEMA. Logical Methods in Computer Science, 2(1), 2006.

6. D. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-dimensional modal logics: theory and applications. Studies in Logic and the Foundations of Mathematics, 148. Elsevier, 2003.

7. D. Gabbay and V. Shehtman. Products of modal logics, part 1. Journal of the IGPL, 6:73-296, 1998.

8. D. Gabbay, V. Shehtman, and D. Skvortsov. Quantification in Nonclassical Logic. Studies in Logic and the Foundations of Mathematics, 153. Elsevier, 2009.

9. R. Goldblatt and S. Thomason. Axiomatic classes in propositional modal logic. In Algebra and Logic, Lecture Notes in Math., Vol. 450, pages 163-173. Springer, Berlin, 1974.

10. V. Goranko and D. Vakarelov. Sahlqvist formulas unleashed in polyadic modal languages. In Advances in Modal Logic 3, pages 221-240. King's College Publications, 2000.

11. V. Goranko and D. Vakarelov. Elementary canonical formulae: extending Sahlqvist's theorem. Annals of Pure and Applied Logic, 141(1-2):180-217, 2006.

12. G. Governatori, I. Hodkinson, and Y. Venema, editors. Advances in Modal Logic 6, papers from the sixth conference on "Advances in Modal Logic," held in Noosa, Queensland, Australia, on 25-28 September 2006. King's College Publications, 2006.

13. L. Henkin, J. Monk, and A. Tarski. Cylindric algebras, part I. North-Holland, 1971.

14. I. Hodkinson. Hybrid formulas and elementarily generated modal logics. Notre Dame Journal of Formal Logic, 47(4):443-478, 2006.

15. JI. JI. Максимова, Д. П. Скворцов, и В. Б. Шехтман. Невозможность конечной аксиоматизации логики финитных задач Медведева. Доклады АН СССР, 245(5): 1051-1054, 1979.

16. С. Кикоть. Об аксиоматике модальных логик квадратов шкал Крипке с выделенной диагональю. В Тезисы докладов секции "Математика и механика" Международной конференции студентов, аспирантов и молодых ученых "Ломоносов-2009", pages 33-34, 2009.

17. С. Кикоть. О квадратах модальных логик с выделенной диагональю. Математические заметки, 88(2):261-274, 2010.

18. С. Кикоть. О модальной определимости некоторых формул первого порядка. Рукопись депонирована в ВИНИТИ 29.04.2010, №234-В2010, Указатель №6, 2010.

19. S. Kikot. Formulas, corresponding to diagrams. In International Conference "Computer science applications of modal logic". Abstracts, pages 18-19. Independent University of Moscow, 2005.

20. S. Kikot. A new generalization of Sahlqvist theorem. In Algebraic and Topological Methods in Non-classical Logics II, Abstracts, Universitat de Barcelona, pages 40-41, Barcelona, 2005.

21. S. Kikot. An extension of Kracht's theorem to generalized Sahlqvist formulas. Journal of Applied Non-Classical Logic, 19/2:227-251, 2009.

22. S. Kikot. Semantic characterization of Kracht's formulas. In Advances in Modal Logic 8, pages 218-234, 2010.

23. M. Kracht. How completeness and correspondence theory got married. In M. de Rijke (Ed.), Diamonds and Defaults, pages 175-214. Synthese Library, Kluwer, 1993.

24. M. Kracht. Tools and Techniques in Modal Logic. Studies in Logic and the Foundations of Mathematics, 142. Elsevier, 1999.

25. S. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 24, No 1:1-14, 1959.

26. A. Kurucz. On axiomatising products of Kripke frames. Journal of Symbolic Logic, 65:923-945, 2000.

27. A. Kurucz. On axiomatising products of Kripke frames, part II. In C. Areces and R. Goldblatt, editors, Advances in Modal Logic 7, pages 219-230. King's College Publications, 2008.

28. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Proceedings of the Third Scandinavian Logic Symposium, Amsterdam, North-Holland, pages 110-143, 1975.

29. G. Sambin and V. Vaccaro. Topology and duality in modal logic. Annals of Pure and Applied Logic, 37:249-296, 1988.

30. G. Sambin and V. Vaccaro. A topological proof of Sahlqvist's theorem. Journal of Symbolic Logic, 54:992-999, 1989.

31. V. Shehtman. On some two-dimensional modal logics. In 8th International Congress on Logic, Methodology, and Philosophy of Science. Abstracts, volume 1, pages 326330. Moscow, 1987.

32. D. Vakarelov. Extended Sahlqvist formulae and solving equations in modal algebras. In 12-th International Congress of Logic Methodology and Philosophy of Science, August 7-13. Abstracts, page 33. Oviedo, Spain, 2003.

33. Y. Venema. Many-dimensional modal logic. PhD thesis, University of Amsterdam,

34. E. Zolin. Query answering based on modal correspondence theory. In Proceedings of the 4th "Methods for modalities" Workshop (M4M-4), pages 21-37, 2005.

35. В. Б. Шехтман. Двумерные модальные логики. Математические заметки, 23(5):759-773, 1978.

36. JI. Л. Эсакиа. Топологические модели Крипке. Доклады АН СССР, 214(2):298-301, 1974.1991.