Модальные логики с нестандартными модальностями тема диссертации и автореферата по ВАК РФ 09.00.07, кандидат философских наук Шкатов, Дмитрий Петрович

• Шкатов, Дмитрий Петрович
• кандидат философских наук
• 2006

Оглавление диссертации кандидат философских наук Шкатов, Дмитрий Петрович

Введение

1 Модальная логика и гардидные фрагменты 13 1.1 Модальная логика и первопорядковая логика ф 1.2 Модальная логика в сравнении с первопорядковой логикой

1.3 Первопорядковые гардидные логики 1.4 Гардидные логики более высоких порядков

2 Интуиционистские модальные логики

2.1 Введение

2.2 Двух-переменный монадический гардидный фрагмент

2.3 Условия замкнутости

2.4 Интуиционистские модальные логики

2.5 Погружение в двух-переменный монадический фрагмент

2.6 Разрешимость

2.7 Примеры

3 Логики с оператором Сегерберга

3.1 Введение

3.2 Язык 78 ф 3.3 Нормальные логики

3.4 Логика Seg 3.5 Расширения Seg

4 Логики с экзистенциальной модальностью

4.1 Логики К#и DK#

4.2 Логики PDWath и PDLpa£/l без связанности

Введение диссертации (часть автореферата) на тему «Модальные логики с нестандартными модальностями»

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

Актуальность темы. Хотя модальная логика—это давно появившаяся и к настоящему времени достаточно хорошо развитая область исследований и "стандартные" модальные логики были тщательно изучены (в чем можно убедиться, пролистав фундаментальную монографию [26], посвященную модальным логикам), в недавнее время в литературе были сформулированы логики, модальности которых не были изучены исследователями модальных логик. Достаточно часто эти "нестандартные" модальности появляются в результате попыток применить аппарат модальных логик к моделированию явлений, изучаемых в различных областях знания; иначе говоря, их рассмотрение мотивировано нуждами прикладной модальной логики, то есть той области логики, которая изучает логические системы, изначально мотивируемые рассмотрением феноменов, изучаемых в различных областях знания, не обязательно (но не исключая) философского. Неудивительно, что прикладные исследования приводят к возникновению модальностей, не изученных в исследованиях, которые имели главным образом философскую и математическую мотивацию.

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

Первый класс логик, рассматриваемых в настоящей диссертации—это интуиционистские модальные логики, то есть модальные логики, немодальной основой которых является интуиционистская логика. Хотя исследования итуиционист-ских (главным образом, не-модальных, но отчасти и модальных) логик, мотивированные проблемами из области оснований математики, имеют долгую и богатую историю, в 90-х годах интерес к интуиционистским модальным логикам резко возрос, так как оказалось, что они могут быть использованы для формального моделирования широкого класса явлений, изучаемых прикладными логиками, главным образов явлений из области теоретической компыотеристики. В частности, значительный интерес к интуиционистским модальным логикам привлекли исследования Могги [72] в области А-исчислений с типами, пополненных конструкциями, называемыми монадами. Логикам давно было известно, что существует соответствие между А-исчислением с типами и интуиционистской модальной логикой через так называемый изоморфизм Карри-Ховарда, отображающий А-термы в формулы интуиционистской логики. С точки зрения прикладной логики, это означает, что интуиционистская логика—это полезный инструмент для построения выводов в области формальной семантики функциональных языков программирования, которая обычно формулируется в терминах А-исчисления с типами. Могги расширил А-исчисление с типами, добавив к нему конструкции, названные им монадами, призванные моделировать те черты функциональных языков программирования (например, исключения), которые не могут быть смоделированы в "чистом" А-исчислении. При попытке найти логический "напарник" такого расширенного А-исчисления оказалось, что ему соответствует интуиционистский аналог логики S4, хорошо известной из области классических модальных логик. Это открытие вызвало шквал работ, посвященных интуиционистской S4, ее теории доказательств, категорией и крипкеской семантикам (см., например, [20], [17], [42], [62], [79], [4], [27], [28], [78]). Помимо этого, интуиционистские модальные логики были использованы для моделирования неполной информации (см. [96]), систем коммуникации (см. [90]) и методов проверки компьютерного оборудования (см. [70], [33]). С точки зрения упомянутых приложений, особый интерес представляет (исследуемая в настоящей диссертации) проблема разрешимости интуиционистских модальных логик, так как логики с неразрешимой проблемой выполнимости, хотя могут представлять некий теоретический интерес, практически совершенно непригодны.

Второй класс логик, рассматриваемый в настоящей диссертации—это логики с оператором конечной итерации ф . Мы рассматриваем логики с ф с точки зрения, отличной от точки зрения, с которой мы рассматриваем интуиционистские модальные логики. В то время как интуиционистские модальные логики, рассматриваемые в диссертации, определены семантически через наложение условий на отношения достижимости в крипкевских моделях, логики с ф рассматриваются как синтаксически определенный класс (нормальных модальных) логик, минимальный член которого мы называем Seg. Изучение расширений Seg представляется актуальным с двух точек зрения: исторической и прикладной. Исторически, общее изучение логик с оператором Сегерберга является естественным продолжением предшествующих исследований в области модальной логики, которое началось в 1910-х годах с исследования отдельных мономодальных систем и развивалось в дальнейшем в двух главных направлениях. Во-первых, были сформулированы и изучены модальные логики в более сложных языках. В 1950-х годах, А. Прайор исследовал временные логики, имеющие две независимые модальности; в 1970-х, В. Пратт начал исследование логик действий, модальности которых строятся из бесконечного набора базовых модальностей при помощи операторов, заимствованных из алгебры регулярных выражений, в том числе оператора конечной итерации—как позже выяснилось, это было только самым началом почти неостановимого размножения модальностей, которое имело место в 1980-х и 1990-х годах и которое продолжается до сих пор: почти любое новое приложение модальных логик порождало новые, доселе неизученные модальности (достаточно подробный обзор "новых модальностей" может быть найден в [36]). Во-вторых, в 1960-х, ввиду лавинообразного увеличения числа приложений модальной логики как в философии, так и за ее пределами, исследователи начали изучать не отдельные системы модальных логик, а целые классы таких систем: нереалистично ограничивать наше внимание несколькими модальными системами в надежде на то, что прикладники найдут среди изученных нами систем то, что им нужно; более реалистично изучать классы модальных систем с тем, чтобы мы могли описать логику, требуемую в новом приложении на основе того (изученного нами) класса логик, к которому она принадлежит. Таким образом, изучение классов модальных логик становится первостепенной проблемой. Такой массовый (или метаметатеоретический) подход к изучению модальных логик в настоящее время лучше всего разработай для простейшего случая—мономодальных логик (см. [26]). Логики с более сложными модальностями изучались по-системно до середы 1990-х, когда Ф. Вольтер стал применять массовый подход к изучению временных логик (см. [105], [104], [102], [103], [100]). Следующим шагом было бы логично расширить такой подход на изучение логик с оператором конечной итерации ф ; первый шаг в этом направлении предпринимается в настоящей диссертации. С точки зрения практических приложений, изучение логик с ф мотивировано тем, что понятие конечной итерации появляется в формальном моделировании очень широкого круга явлений. Мы приведем только два примера. В теоретической компьютеристике ф моделирует повторное выполнение программ (например, в петлях); для формального описания программ компыотеристы-теоретики используют логику PDL, язык которой содержит <$> и которая строится на основе полимодального варианта логики К. Несмотря на то, что PDL и некоторые ее варианты хорошо изучены, никто не изучал, что происходит в случае добавления PDL-модальностей к произвольным моно- и полимодальным логикам. Массовый подход к изучению логик программ расширил бы паше понимание логических свойств программ в контекстах, в которых мы хотели бы потребовать, чтобы базисные (или атомарные) программы обладали бы какими-то специальными свойствами (например, свойством Черча-Россера, которое постулируеися в А-исчислении и которое используется для построения формальных семантик программ). Другая область, в которой понятие конечной итерации играет ключевую роль и в которой логическое моделирование является одним из основных методов исследования—это изучение знания в мульти-агентных системах, то есть в формальных моделях совокупности взаимодействующих познающих субъектов, в которых оператор конечная итерация используется для формального моделирования так называемого "общего знания", то есть знания о некотором факте, которое доступно всем познающим субъектам, наряду со знанием о самой этой доступности (см. [32]).

Третья группа логик, рассматриваемых в настоящей диссертации,—это логики с экзистенциальной модальностью (#), называнной нами так потому, что в семантике крипкевского типа формула (#) ip означает, что существует некоторое (атомарное) отношение достижимости Ra такое, что формула ip истинна в точке, достижимой по Ra. Эта модальность совсем недавно привлекла внимание логиков-прикладников в контексте логического моделирования полуструктурированных данных (см. [9]). Полуструктурированными называют данные, которые имеют определенную структуру, но не настолько строгую, как базы данных; мотивирующий пример полуструктурированных данных—сеть Интернет (см. [1]). Полуструктурированные данные обычно моделируют при помощи графов с отмеченными ребрами (то есть графов, в которых не только узлы, но и ребра имеют имена). Для рассуждения о полуструктурированных данных в литературе был предложен широкий круг формальных языков. Многие из этих языков оказались вариантами модальных языков (что неудивительно, поскольку графы могут быть естественным образом рассмотрены как крипкевские модели). В частности, в [9] для рассуждений о полуструктурированных была предложена модальная логика PDLpu"'. Модальность (#), одна из модальностей языка PDLJ'ut/l, естественным образом возникает в контексте полуструктурированных данных (например, рассуждая о сети Интернет, мы часто хотим иметь возможность сказать в используемом нами формальном языке, что какая-то интернет-страница достижима из другой интернет-страницы по какой-то ссылке, и нам не важно, как эты ссылка обозначена на ссылающейся странице).

Степень разработанности проблемы. Поскольку интуиционистские модальные логики возникали главным образом в исследованиях по прикладной логике, где различные прикладные области порождают различные логические системы, это привело в возникновению огромного числа интуиционистских модальных логик, отличающихся между собой не только тем, как модальности взаимодействуют с немодальными связками, но и самими определениями модальных связок. Эта ситуация резко отличается от ситуции, имеющей место в классической модальной логике, где все исследователи согласны в том, как должны определяться модальные связки. Такой "разброс и шатание" означают, что доказательство любых достаточно общих результатов об интуиционистских модальных логиках является довольно-таки затруднительным. В частности, нелегко сформулировать достаточно общий метод доказательства разрешимости интуиционистских модальных логик. До настоящего времени, единственный метод обоснования разрешимости интуиционистских модальных логик, предложенный в литературе—это погружение интуиционистских модальных логик с п модальностями в классические модальные логики (называемые классическими "напарниками" интуиционистских логик) с п+1 модальностями, предложенное Ф. Вольтером и М. Захарьящевым (см. [98], [97], [99]). Метод Вольтера и Захарьящева имеет строгое ограничение: он может быть использован для обоснования разрешимости только тех интуиционистских логик, разрешимость чьих классических напарников нам уже известна. Общих методов доказательства разрешимости интуиционистских модальных логик, не зависящих от известности нам разрешимости их классических напарников, в литературе предложено не было.

Что касается второго класса логик, исследуемых в диссертации, класса расширений минимальной нормальной логики с оператором ф , следует заметить, что несмотря на то, что сам оператор ф давно известен (он был введен в 1970-х годах В. Праттом, см. [81]) и аксиоматически охарактеризован (см. [86]), исследованием класса расширений минимальной нормальной логики с ф до настоящего времени никто не занимался.

Что касается логик с экзистенциальной модальностью (#), то модальность (#) привлекла внимание логиков совсем недавно и к настоящему времени единственной работой, посвященной логикам с (#), является [9], где семантически определяется и изучается логика PDWath. Важно отметить, что для практических применений PDLpat/l, для которых она была предложена (рассуждения о полуструктурированных данных) существенно важно наличие дедуктивной системы, позволяющей обосновать те (и только те) выоды, которые законны в PDLpaf/l; однако, в настоящее время работы, посвященные аксиоматизации PDLpaf'1, в литературе отсутствуют.

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

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

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

• Построение непротиворечивой и полной аксиоматизации логики PDL*"1"' и ряда связанных с ней логик.

Научная новизна работы. В диссертации впервые выполнены следующие задачи:

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

• Построена альтернативная семантика гардидного фрагмента и доказана ее адекватность стандартной первопорядковой семантике.

• Приведено теоретико-модельное доказательство разрешимости базисного гардидного фрагмента первопорядковой логики методом мозаик.

• Сделан обзор основных результатов области в гардидных фрагментов.

Доказано обобщение результата Ганцингера, Мейера и Винеса (см. [38]) о разрешимости двух-переменного монадического гардидного фрагмента первопорядковой логики GF^l0Tl с условиями замкнутости, выразимыми в монадической второпорядковой логике, наложенными на отношения, обозначенные предикатными параметрами GF^-формул, на фрагмент, в котором на отношения, обозначенные предикатными параметрами GF?n(m-формул, может быть наложено более одного условия.

Разработан новый метод доказательства разрешимости интуиционистских модальных логик через погружение в GF^^, в котором на отношения, обозначенные предикатными параметрами, наложены условия замкнутости, выразимые в монадической второпорядковой логике, и показано, что этот метод может быть использован для доказательства разрешимости широкого класса известных из литературы интуиционистских модальных логик.

Доказан аналог теоремы Макинсона для логик с оператором конечной итерации ф .

Доказано, что логики с ф имеют конечные нестандартные модели.

Доказано, что добавление аксиом, характеризующих ф , к логике S4 дает систему, эквивалентную S4.

Доказано, что добавление аксиом, характеризующих ф , к произвольной мономодальной логике А дает консервативное расширение А.

Сформулирован стандартный перевод формул логик с (#) в гардидный фрагмент логики с оператором наименьшей неподвижной точки.

Построены аксиоматизации гильбертовского типа минимальной нормальной логики с экзистенциальной модальностью (#), ее детерминистичекого расширения, логики PDU"^'1 и одного из ее вариантов; доказана их семантическая адекватность и полнота.

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

• разрешимость двух-переменного монадического гардидного фрагмента пер-вопорядковой логики GF^ с условиями замкнутости, выразимыми в мо-надической второпорядковой логике, доказана путем сведения проблемы выполнимости формул этого фрагмента к проблеме выполнимости формул теории SkS (монадической второпорядковой теории деревьев с постоянным фактором ветвления к)]

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

• аналог теоремы Макинсона для логик с ф доказывается через преобразование канонических моделей этих логик;

• полнота логик с оператором (#) доказывается через построение конечных канонических моделей для этих логик.

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

• Доказано обобщение результата Ганцингера, Мейера и Винеса (см. [38]) о разрешимости двух-переменного монадического гардидного фрагмента первопорядковой логики GF^ с условиями замкнутости, выразимыми в монадической второпорядковой логике, наложенными на отношения, обозначенные предикатными параметрами G/^„-формул, на фрагмент, в ко-тром на отношения, обозначенные предикатными параметрами GFjum-формул, может быть наложено более одного условия.

• Разработан новый метод доказательства разрешимости интуиционистских модальных логик через погружение в GF?non, в котором на отношения, обозначенные предикатными параметрами, наложены условия замкнутости, выразимые в монадической второпорядковой логике, и показано, что этот метод может быть использован для доказательства разрешимости широкого класса известных из литературы интуиционистских модальных логик.

• Доказан аналог теоремы Макинсона для логик с оператором конечной итерации ф •

• Сформулирован стандартный перевод формул логик с (#) в гардидный фрагмент логики с оператором наименьшей неподвижной точки и тем самым доказана разрешимость логик с (#), семантически определимых при помощи гардидных формул.

• Построены аксиоматизации гильбертовского типа минимальной нормальной логики с экзистенциальной модальностью (#), ее детерминистичекого расширения, логики PD\palh и одного из ее вариантов; доказана их семантическая адекватность и полнота.

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

• Предложенный нами общий метод доказательства разрешимости интуиционистских модальных лоик может быть использован для доказательства разрешимости конкретных систем интуиционистской модальной логики.

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

• Построенные нами аксиоматизации логик с (#) могут лечь в основу написания программ автоматического поиска доказательств в этих логиках.

Кроме того, материал диссертации может быть использован при разработке спецкурсов по модальной логике для специализирующихся по кафедрам логики философских факультетов. Следует отметить, что несмотря на то, что логики, рассматриваемые в настоящей диссертации, были сформулированы в исследованиях по прикладной, а не философской, логике, как мы неоднократо подчеркиваем в основном тексте диссертации, эти логики представляют непосредственный интерес для философского логика. Так, интуиционистские модальные логики представляют непосредственный интерес для тех логиков-философов, которые полагают, что основу систем формальной логики должна составлять не классическая, а интуиционистская концепция истинности. Проект построения и исследования интуиционистских систем пока не продвинулся далеко за пределы базовой интуиционистской логики, и исследование интуиционистских модальных логик является естественным следующим шагом в этом направлении. Логики с оператором конечной итерации представляют непосредственный интерес для исследователей в областях логики действий и логики знаний, в которых оператор конечной итерации играет ключевую роль. Наконец, логики с экзистенциальной модальностью также представлояют непосредственный интерес для исследователей действий и логик знаний, так как они дают нам возможность рассуждать о знаниях, которыми обладают какие-то, возможно неизвестные, субъекты знания и о высказываниях, истинностный статус которых может быть изменен при помощи какого-то, возможно неизвестного нам, действия. Представляется, что на настоящем этапе развития логики прикладная логика выполняет для философской логики ту же функцию, которую исследования по основаниям математики выполняли в первой половине 20-го века: ставя перед исследователями конкретные, осязаемые проблемы, прикладная логика дает точок развитию логического аппарата, который затем, вторично, используется логиками, анализирующими философские проблемы.

Структура диссертации. Настоящая диссертация структурирована следующим образом. В главе 1 мы излагаем материал, касающийся модальных логик и гардидных фрагментов логик первого и более высоких порядков, на который мы будем опираться в последующих главах диссертации1. В главе 2 мы излагаем общий метод доказательства разрешимости интуиционистских модальных логик. В главе 3 мы доказываем ряд результатов о классе логик с оператором конечной итерации. Наконец, в главе 4 мы формулируем аксиоматизации гильбертовского типа логики PDLpat/l и ряда связанных с ней логик и доказываем их полноту. различных разделах настоящей диссертации мы доказываем результаты о разрешимости различных модальных логик через погружение в различные (разрешимые) гардидные фрагменты логик первого и более высоких порядков. Гардидные фрагмент возникли как результат понимания того, что пропозициональные модальные и первопорядковые языки могут рассматриваться как альтернативные языки для описания реляционных структур и что, следовательно, модальная логика может рассматриваться как фрагмент первопорядковой логики, а не как расширение пропозициональной классической логики в направлении, отличном от первопоряд-кового. Это, в свою очередь, породило желание расширить "модальный фрагмент" первопорядковой логики настолько, насколько это возможно, без потери "хороших" свойств модального фрагмента, прежде всего разрешимости. Это привело к открытию гардидного фрагмента первопорядковой логики (см. [13]), расширяющего фрагмент, который можно назвать базовым модальным фрагментом первопорядковой логики, то есть фрагмент, эквивалентный модальной логике с 0-подобными модальностями. Изучение логик, не погружаемых в гардидный фрагмент (например, логик с модальностью "до тех пор, пока ."), привело к открытию более богатых гардидных фрагментов, в том числе фрагментов логик, более богатых, чем перво-порядковая, например логики с оператором наименьшей неподвижной точки. Таким образом, гардидные фрагменты являются обобщениями различных модальных логик и могут рассматриваться как "максимальные (по своим выразительным возможностям) модальные логики". В частности, погружаемость логики в тот или иной гардидный фрагмент может служить обоснованием ее модального характера.

Заключение диссертации по теме «Логика», Шкатов, Дмитрий Петрович

Заключение

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

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

В главе 3 мы доказали достаточно общий результат о разрешимости интуиционистских модальных логик путем погружения этих логик в двух-переменный монадический гардидный фрагмент GF^non с ацикличными множествами условий закмкнутости, определимыми в монадической второпорядковой логике, наложенными на отношения, обозначенные предикатными параметрами GF^m-формул. Разрешимость этого фрагмента была доказана в главе 3 путем обобщения результата из [38] о разрешимости GF^l0n с единственным условием закмкнутости, определимыми в монадической второпорядковой логике, наложенными на одно из отношений, обозначенных предикатными параметрами СРД^-формул, а не множеств таких условий (обобщение результата из [38] на множества условий понадобилось нам для доказательства разрешимости тех интуиционистских модальных логик, в семантике которых на отношения достижимости наложено более одного условия). Наш результат обосновывает разрешимость значительного числа известных интуиционистских модальных логик. В частности, мы доказали (теорема 2.17 и пример 2.18), что наш результат обосновывает разрешимость интуиционистских модальных логик, определенных следующими множествами условий (эти условия являются наиболее популярными в литературе по интуиционистским модальным логикам): {TZ о TZ$ oTZ = TZ$,TZ о 7Zq о 7Z = IZn} и {7г0 С 7Z). Метод, использованный нами для доказательства разрешимости, преодолевает ограничение единственного до настоящего времени предложенного общего метода доказательства разрешимости интуиционистских модальных логик, использованного в работах [98], [97], [99], в которых разрешимость доказывается через погружение интуиционистских модальных логик с п модальностями в разрешимые классические модальные логики сп + 1 модальностями (эти классические логики называются классическими напарниками интуиционистских логик). Ограничение такого метода доказательства разрешимости заключается в том, что он может быть использован для доказательства разрешимости только тех интуиционистских модальных логик, разрешимость чьих классических напарников нам уже известна. Наш метод не имеет этого ограничения. Однако, наш метод имеет другое ограничение: для доказательства разрешимости логики Л нашим методом мы должны суметь переформулировать условия, наложенные на отношения достижимости в крипкевской семантике Л таким образом, чтобы они имели вид условий замкнутости, определимых в монадической второпорядковой логике. Как мы уже упоминали в главе 3, мы не смогли выполнить требуемую переформулировку для ряда известных интуиционистских модальных логик: логики IS4, сформулированной в [89], и логик, среди семантических условий которых имеется условие TZq о TZ С TZ о TZa- Соответственно, расширение метода, предложенного в главе 3, на упомянутые логики (то есть, либо успешная попытка переформулировать семантические условия упомянутых логик как условия замкнутости, определимые во второпорядковой монадической логике, или обобщение самого метода) является наиболее актуальным направлением дальнейших исследований.

В главе 4 мы доказали аналог теоремы Макинсона (а также несколько менее значительных результатов, таких как консервативность отностителыю мономодальних логик и существование конечных нестандартных моделей) для решетки расширений логики Seg, которая является логикой, полученной из базовой (классической) модальной логики К* в языке, содержащем две модальности, 0 и ф (называемую в главе 4 "оператором Сегерберга"), добавлением аксиом, придающим модальнойсти ф значение оператора конечной итерации. Аналог теоремы Макинсона для решетки расширений Seg—это небольшой первый шаг в исследовании решетки расширений Seg. Задача исследования этой решетки логик выглядит довольно-таки объемной и трудной; поэтому, было бы разумно в качестве следующего шага в исследовании расширений Seg изучить табличные расширения Seg (то есть, расширения, для которых имеется конечная характеристическая матрица, подобная хорошо известным таблицам истинности для классической пропозициональной логики). Было бы логично вслед за доказательством аналога теоремы Макинсона, осуществленным в главе 4, попытаться доказать аналог "обобщения теоремы Макинсона", доказанный для мономодальных логик А. В. Чагровым в [109]: для всякого эффективно конечно-аксиоматизируемого табличного расширения А логики К—за исключением логик шкалы, состоящей из одной рефлексивной точки, и шкалы, состоящей из одной иррефлексивной точки,—и произвольной формулы ф, неразрешимо, совпадает ли логика, полученная добавлением ip к К, с А.

В главе 5 мы сформулировали исчисления гильбертовского типа (и доказали их полноту) четырех логик, язык которых содержит экзистенциальную модальность (#) (то есть, модальность, которая может "сказать", что формула истинна в точке модели, достижимой по какому-то атомарному отношению достижимости); а именно, мы сформулировали аксиоматизировали минимальную логику с (#), названную нами К#, ее детерминистическое расширение, названное нами DK#, логику PDLpath, сформулированную в [3], и вариант PDLput'', получаемый за счет выбрасывания из семантического определения PDLpat/l условия связанности моделей. Следующим шагом в изучениии логик с (#) было бы логично аксиоматизировать детерминистическое расширение PDU"1"1, то есть расширение PDLpui/l, семантически определенное через ограничение класса шкал логики PDLpat/l шкалами, где все атомарные отношения достижимости должны быть детерминистическими.

Список литературы диссертационного исследования кандидат философских наук Шкатов, Дмитрий Петрович, 2006 год

1. S. Abiteboul, P. Buneman, and D. Suciu. Data on the Web. Morgan Kaufmann, 2000.

2. N. Alechina. On A Decidable Generalized Quantifier Logic Corresponding to a Decidable Fragment of First Order Logic. Journal of Logic, Language and Information, 4:177 189, 1995.

3. N. Alechina and D. Shkatov. On decidability of intuitionistic modal logics. In Proceedings of the Third Workshop Methods for Modalities (МЩ), 2003.

4. N. Alechina and D. Shkatov. Survey of guarded logics. Technical Report NOTTCS-TR-2004-10, School of Computer Science and IT, University of Nottingham, 2004.

5. N. Alechina and D. Shkatov. A general method for proving decidability of intuitionistic modal logics. Journal of Applied Logic, 2005.

6. Natasha Alechina, Maarten de Rijke, and Stdphane Demri. A modal perspective on path constraints. Journal of Logic and Computation, 13(6):939-956, 2003.

7. Natasha Alechina and Neil Immerman. Reachability logic: An efficient fragment of transitive closure logic . Logic Journal of IGPL, 8(3):325-337, 2000.

8. H. Andr6ka, J. van Benthem, and I. №meti. Modal Languages and Bounded Fragments of Predicate Logic. Technical Report ML-96-03, ILLC, University of Amsterdam, 1996.

9. Hajnal Andr6ka, Johan van Benthem, and Istvdn N6meti. Back and forth between modal logic and classical logic. Bulletin of the Interest Group in Pure and Applied Logics, 3:685-720,1995.

10. Hajnal And^ka, Johan van Benthem, and Istv&n Ndmeti. Modal logics and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998.

11. J. Benthem, van. Modal logic and classical logic. Bibliopolis, Naples, 1983.

12. J. Benthem, van and N. Alechina. Modal quantification over structured domains. In M. de Rijke, editor, Advances in Intensional Logic, pages 1 -27. Kluwer, Dordrecht, 1997.

13. N. Benton, G. Bierman, and V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177-193, 1998.

14. Dietmar Berwanger and Achim Blumensath. Automata for guarded fixed point logics. In E. Gradel, W. Thomas, and T. Wilke, editors, Automata, Logics, and Infinite Games, number 2500 in LNCS, chapter 19, pages 343-355. Springer Verlag, 2002.

15. G. M. Bierman and V. de Paiva. On an intuitionistic modal logic. Studia Logica, 65(3):383-416, 2000.

16. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 2001.

17. E. Borger, E. Gradel, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag, 1997.

18. R. A. Bull. A modal extension of intuitionistic modal logic. Notre Dame Journal of Formal Logic, VI(2):142-146, 1965.

19. R. A. Bull. Some modal calculi based on 1С. In Formal Systems and Recursive Functions, pages 3-7. North Holland, 1965.

20. R. A. Bull. MIPC as the formalisation of an intuitionistic concept of modality. Journal of Symbolic Logic, 31(4):609-616, 1966.

21. Alexander Chagrov and Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997.

22. R. Davies and F. Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proc. of 23rd POPL, pages 258-270. ACM Press, 1996.

23. R. Davies and F. Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, 2001.

24. G. De Giacomo. Decidability of Class-Based Knowledge Representation Formalisms. PhD thesis, Universitd degli Studi di Roma "La Sapienza", 1995.

25. Hans de Nivelle and Maarten de Rijke. Deciding the guarded fragments by resolution. Journal of Symbolic Computation, 35(1):21—58, January 2003.

26. K. Dosen. Models for stronger normal intuitionistic modal logics. Studia Logica, 44:39-70, 1985.

27. Ronald Fagin, Jeseph Y. Halpern, and Moshe Vardi. Reasoning about Knowledge. MIT Press, 1995.

28. M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137(1):1 33, 1997.

29. G. Fisher Servi. On modal logics with intuitionistic base. Studia Logica, 27:533546, 1986.

30. F. B. Fitch. Intuitionistic modal logic with quantifiers. Portugaliae Mathematicae, 7:113-118, 1948.

31. Dov Gabbay, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications. Elsever, 2003.

32. Harald Ganzinger and Hans De Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proc. 14th IEEE Symposium on Logic in Computer Science, pages 295-305. IEEE Computer Society Press, 1999.

33. Harald Ganzinger, Christoph Meyer, and Margus Veanes. The two-variable guarded fragment with transitive relations. In Proc. 14 th IEEE Symposium on Logic in Computer Science, pages 24-34. IEEE Computer Society Press, 1999.

34. R. Goldblatt. Metamathematics of modal logic. Reports on mathematical Logic, 6,7:31 42, 21 - 52, 1976.

35. Elisabeth Gongalvfcs and Erich Gradel. Decidability issues for action guarded logics. In Proceedings of 2000 International Workshop on Description Logics -DL2000, pages 123-132, 2000.

36. G. Gottlob, E. Gradel, and H. Veith. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic, 3(l):l-35, 2002.

37. J. Goubault-Larrecq. Logical foundations of eval/quote mechanisms, and the modal logic S4. Manuscript, 1996.

38. Erich Gradel. Decision procedures for guarded logics. In Automated Deduction CADE16. Proceedings of 16th International Conference on Automated Deduction, Trento, 1999, volume 1632 of LNCS. Springer-Verlag, 1999.

39. Erich Gradel. On the restraining power of guards. Journal of Symbolic Logic, 64:1719-1742, 1999.

40. Erich Gradel. Guarded fixed point logic and the monadic theory of trees. Theoretical Computer Science, 288:129-152, 2002.

41. Erich Gradel. Decidable fragments of first-order and fixed-point logic. From prefix-vocabulary classes to guarded logics. In Proceedings of Kalmar Workshop on Logic and Computer Science, Szeged, 2003.

42. Erich Gradel, Colin Hirsch, and Martin Otto. Back and Forth Between Guarded and Modal Logics. In Proceedings of 15th IEEE Symposium on Logic in Computer Science LICS 2000, pages 217-228, Santa Barbara, 2000. See also: journal version 50].

43. Erich Gradel, Colin Hirsch, and Martin Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, 3(3):418 -463, 2002. See also: conference version 49].

44. Erich Gradel and Igor Walukiewicz. Guarded Fixed Point Logic. In Proceedings of 14th IEEE Symposium on Logic in Computer Science LICS '99, Trento, pages 45-54, 1999.

45. David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000.

46. L. Henkin, J. D. Monk, A. Tarski, H. Andr6ka, and I. N6meti. Cylindric set algebras. Springer Verlag, 1981.

47. Colin Hirsch and Stephan Tobies. A tableau algorithm for the clique guarded fragment. In Proceedings of the Workshop Advances in Modal Logic AiML 2000, Leipzig, Germany, 2000.

48. Ian Hodkinson. Loosely guarded fragment has finite model property. Studia Logica, 70:205 240, 2002.

49. Ian Hodkinson. Monodic packed fragment with equality is decidable. Studia Logica, 72:185-197, 2002.

50. Ian Hodkinson and Martin Otto. Finite Conformal Hypergraph Covers, with Two Applications. Bulletin of Symbolic Logic, 9:387 405, 2003.

51. Eva Hoogland and Maarten Marx. Interpolation in guarded fragments. Studia Logica, 70(3):373-409, 2002.

52. George H. Hughes and Michael J. Cresswell. A New Introduction to Modal Logic. Routledge, 1996.

53. S. Kobayashi. Monad as modality. Theoretical Computer Science, 175:29 74, 1997.

54. Clarence I. Lewis and Cooper H. Langford. Symbolic Logic. Dover, 1932.

55. C. Lutz, U. Sattler, and L. Tendera. The complexity of finite model reasoning in description logics. In Proc. of the 19th Conference on Automated Deduction (CADE-19), volume 2741 of Lecture Notes in Artificial Intelligence. Springer Verlag, 2003.

56. David C. Makinson. Some embedding theorems for modal logic. Notre Dame Journal of Formal Logic, pages 252-254, 1971.

57. Maarten Marx. Tolerance logic. Journal of Logic, Language and Information, 10:353-373, 2001.

58. Maarten Marx, Stefan Schobach, and Szabolcs Mikulas. Labelled Deduction, chapter Labelled deduction for the guarded fragment. Applied Logic Series. Kluwer, 2000.

59. Gregory McColm. Guarded quantification in least fixed point logic. Journal of Logic, Language and Information, to appear.

60. E. Mendelson. An introduction to mathematical logic. Van Nostrand Reinhold, 1979.

61. M. Mendler. Constrained proofs: a logic for dealing with behavioural constrains in formal hardware verification. In G. Jones and M. Sheeran, editors, Proceedings of Workshop on Designing Correct Circuits, Oxford 1990. Springer-Verlag, 1991.

62. G. Mints. Some calculi of modal logic. Trudy Matematicheskogo Instituta imeni V.A.Steklova, 98:88-111, 1968.

63. E. Moggi. Notions of computation and monads. Information and Computation, 93(l):55-92, July 1991.

64. Istvan Nemeti. Decidability of weakened versions of first order logic and cylindric relativized set algebras. In L. Csirmaz, D. M. Gabbay, and M. de Rijke, editors, Logic Colloquium'92. CSLI, 1992.

65. H. Ono. On some intuitionistic modal logics. Publications of the Research Institute for Mathematical Science, Kyoto University, 13:55-67, 1977.

66. H. Ono and N.-Y. Suzuki. Relations between intuitionistic modal logics and intermediate predicate logics. Reports on Mathematical Logic, 22:65-87, 1988.

67. Martin Otto. Modal and Guarded Characterisation Theorems over Finite Transition Systems. In Proceedings of 17th IEEE Symposium on Logic in Computer Science LICS '02, pages 371-380, 2002.

68. Martin Otto. Modal and Guarded Characterisation Theorems over Finite Transition Systems. Annals of Pure and Applied Logic, 2004. to appear.

69. F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511—540, 2001.

70. A.M. Pitts. Evaluation logic. In G. Birtwistle, editor, IVth Higher Order Workshop, pages 162-189. Springer-Verlag, Banff, 1990.

71. G. D. Plotkin and C. P. Stirling. A framework for intuitionistic modal logic. In J.Y. Halper, editor, Theoretical Aspects of Reasoning about Knowledge, pages 399-406, 1986.

72. Vaughan R. Pratt. Semantical considerations on Floyd-Hoare logic. In 17th Annual Symposium on Foundations of Computer Science, pages 109-121, Houston, Texas, October, 25-27 1976. IEEE.

73. D. Prawitz. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksell, 1965.

74. Arthur Prior. Time and Modality. Oxford University Press, 1957.

75. M. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969.

76. Erich Rosen. Modal logic over finite structures. Journal of Logic, Language and Information, 6:427-439, 1997.

77. Krister Segerberg. A completeness theorem in the modal logic of programme. In T. Traczyk, editor, Universal Algebra and Applications, volume 9 of Banach Center Publications, pages 31-46. PWN-Polish Scientific Publishers, 1982.

78. D. Shkatov. Modal logics with the reflexive-transitive modality. Submitted to Logical Studies, Moscow, Russia.

79. D. Shkatov. Makinson theorem for logics with the reflexive-transitive modality. Logical Studies, 11, 2005. To appear.

80. А. К. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994.

81. C. P. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311-347, 1987.

82. Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev. Speaking about transitive frames in propositional languages. Journal of Logic, Language, and Computation, 7:317 339, 1998.

83. Johan van Benthem. Exploring logical dynamics. CSLI Publications, 1996.

84. Michiel van Lambalgen. The axiomatization of randomness. Journal of Symbolic Logic, 55:1143-1167, 1990.

85. W3C. XML Path Language (XPath) 1.0. Available from http://www.w3.org/TR/xpath.

86. D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic, 50:271-301, 1990.

87. F. Wolter and M. Zakharyaschev. On the relation between intuitionistic and classical modal logics. Algebra and Logic, 36:121-155, 1997.

88. F. Wolter and M. Zakharyaschev. Intuitionistic modal logics. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundations of Mathematics, pages 227-238. Kluwer Academic Publishers, 1999.

89. F. Wolter and M. Zakharyaschev. Intuitionistic modal logics as fragments of classical bimodal logics. In E. Orlowska, editor, Logic at Work, pages 168-186. Springer-Verlag, 1999.

90. Frank Wolter. The finite model property in tense logic. Journal of Symbolic Logic, 60:757-774, 1995.

91. Frank Wolter. A counterexample in tense logic. Notre Dame Journal of Symbolic Logic, 37:167-173, 1996.

92. Frank Wolter. Properties of tense logics. Mathemaical Logic Quaterly, 42:481500, 1996.

93. Frank Wolter. Tense logic without tense operators. Mathematical Logic Quarterly, 42:145-171, 1996.

94. Frank Wolter. Completeness and decidability of tense logics closely related to logics above K4. Journal of Symbolic Logic, 62:131 158, 1997.

95. Frank Wolter. A note on the interpolation property in tense logic. Journal of Philosophical Logic, 26:545-551, 1997.

96. M. Zakharyaschev, F. Wolter, and A. Chagrov. Advanced modal logic. In Dov Gabbay, editor, Handbook of philosophical logic, volume 3, pages 83-266. Kluwer Academic Publishers, 2001.

97. H. А. Алешина и Д.П. Шкатов. О модальных логиках с экзистенциальной модальностью. Логические исследования, 12, 2005.

98. Д. П. Шкатов. Аналог теоремы Макинсона для нормальных модальных логик с оператором Сегерберга. Логические исследования, 11, 2004.

99. А. В. Чагров. Алгоритмическая проблема аксиоматизации табличной нормальной логики. Логические исследования, 9, 2002.