Модальные логики с нестандартными модальностями

Шкатов, Дмитрий Петрович

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

Год: 2006
Автор научной работы: Шкатов, Дмитрий Петрович
Ученая cтепень: кандидата философских наук
Место защиты диссертации: Москва
Код cпециальности ВАК: 09.00.07

Диссертация по философии на тему 'Модальные логики с нестандартными модальностями'

Полный текст автореферата диссертации по теме "Модальные логики с нестандартными модальностями"

РОССИЙСКАЯ АКАДЕМИЯ НАУК ИНСТИТУТ ФИЛОСОФИИ

На правах рукописи

ШКАТОВ Дмитрий Петрович

МОДАЛЬНЫЕ ЛОГИКИ С НЕСТАНДАРТНЫМИ МОДАЛЬНОСТЯМИ

Специальность 09 00 07 Логика

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата философских наук

Москва 2006

Работа выполнена на секторе логики Института Философии Российской Академии Наук

Научный доктор философских наук

руководитель МАРКИН В И

Официальные доктор философских на\ к

оппоненты- ЛЕДНИКОВ Е Е

кандидат философских наук

ЗАЙЦЕВ Д В.

Ведущая Санкт-Петербургский государственный

организация университет, кафедра логики

Защита состоится «2006 года в часов на заседании Диссертационного совета Д 002 29 03 по защите диссертаций на соискание ученой степени доктора философских наук при Институте философии РАН

С текстом диссертации можно ознакомиться в библиотеке Института философии РАН

Автореферат разослан «17.» 2006 г

Ученый секретарь

Диссертационного совета ( Ф М Морозов

кандидат философских наук

Общая характеристика работы

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

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

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

РОС М\Ц.<0Ч\ !. Ы!Б,1! ЛО ! £.. \

годах интерес к интуиционистским модальным логикам резко возрос, так как оказалось, что они могут быть использованы для формального моделирования широкого класса явлений, изучаемых прикладными логиками, главным образов явлений из области теоретической компью-теристики В частности, значительный интерес к интуиционистским модальным логикам привлекли исследования Могги в области А-исчислений с типами, пополненных конструкциями, называемыми монадами Логикам давно было известно, что существует соответствие между А-исчислением с типами и интуиционистской модальной логикой через так называемый изоморфизм Карри-Ховарда, отображающий А-термы в формулы интуиционистской логики С точки зрения прикладной логики это означает, что интуиционистская логика—это полезный инструмент для построения выводов в области формальной семантики функциональных языков программирования, которая обычно формулируется в терминах А-исчисления с типами. Могги расширил А-исчисление с типами, добавив к нему конструкции, названные им монадами, призванные моделировать те черты функциональных языков программирования (например, исключения), которые не могут быть смоделированы в «чистом» А-исчислении. При попытке найти логический «напарник» такого расширенного А-исчисления оказалось, что ему соответствует интуиционистский аналог логики 84, хорошо известной из области классических модальных логик Это открытие вызвало шквал работ, посвященных интуиционистской Я4, ее теории доказательств, категорной и крипкевской семантикам. Помимо этого, интуиционистские модальные логики были использованы для моделирования неполной информации, систем коммуникации и методов проверки компьютерного оборудования С точки зрения упомянутых приложений, особый интерес представляет (исследуемая в настоящей диссертации) проблема разрешимости интуиционистских модальных логик, так как логики с неразрешимой проблемой выполнимости, хотя могут представлять некий теоретический интерес, практически совер- <

шенно непригодны

Второй класс логик, рассматриваемый в настоящей диссертации— это логики с оператором конечной итерации О . Мы рассматриваем

логики с О с точки зрения, отличной от точки зрения, с которой мы рассматриваем интуиционистские модальные логики В то время как интуиционистские модальные логики, рассматриваемые в диссертации, определены семантически через наложение условий на отношения достижимости в крипкевских моделях, логики с О рассматриваются как синтаксически определенный класс (нормальных модальных) логик, минимальный член которого мы называем Seg Изучение расширений Seg представляется актуальным с двух точек зрения: исторической и прикладной. Исторически, общее изучение логик с оператором Сегерберга является естественным продолжением предшествующих исследований в области модальной логики, которое началось в 1910-х годах с исследования отдельных мономодальных систем и развивалось в дальнейшем в двух главных направлениях. Во-первых, были сформулированы и изучены модальные логики в более сложных языках В 1950-х годах, А Прайор исследовал временные логики, имеющие две независимые модальности, в 1970-х годах, В Пратт начал исследование логик действий, модальности которых строятся из бесконечного набора базовых модальностей при помощи операторов, заимствованных из алгебры регулярных выражений, в том числе оператора конечной итерации—как позже выяснилось, это было только самым началом почти неостановимого размножения модальностей, которое имело место в 1980-х и 1990-х годах и которое продолжается до сих пор почти любое новое приложение модальных логик порождало новые, доселе неизученные модальности Во-вторых, в 1960-х годах, ввиду лавинообразного увеличения числа приложений модальной логики как в философии, так и за ее пределами, исследователи начали изучать не отдельные системы модальных логик, а целые классы таких систем нереалистично ограничивать наше внимание несколькими модальными системами в надежде на то, что прикладники найдут среди изученных нами систем то, что им нужно; более реалистично изучать классы модальных систем с тем, чтобы мы могли описать логику, требуемую в новом приложении на основе того (изученного нами) класса логик, к которому она принадлежит Таким образом, изучение классов модальных логик становится первостепенной проблемой Такой мас-

совий (или метаметатеоретический) подход к изучению модальных логик в настоящее время лучше всего разработан для простейшего случая—мономодальных логик Логики с более сложными модальностями изучались по-системно до середы 1990-х годов, когда Ф Вольтер стал применять массовый подход к изучению временных логик Следующим шагом было бы логично расширить такой подход на изучение логик с оператором конечной итерации О , первый шаг в этом направлении предпринимается в настоящей диссертации С точки зрения практических приложений, изучение логик с О мотивировано тем, что понятие конечной итерации появляется в формальном моделировании очень широкого круга явлений Мы приведем только два примера В теоретической компьютеристике <С> моделирует повторное выполнение программ (например, в петлях), для формального описания программ компьютеристы-теоретики используют логику PDL, язык которой содержит О и которая строится на основе полимодального варианта логики К. Несмотря на то, что PDL и некоторые ее варианты хорошо изучены, никто не изучал, что происходит в случае добавления PDL-модальностей к произвольным моно- и полимодальным логикам Массовый подход к изучению логик программ расширил бы наше пони мание логических свойств программ в контекстах, в которых мы хотели бы потребовать, чтобы базисные (или атомарные) программы обладали бы какими-то специальными свойствами (например, свойством Черча-Россера, которое постулируется в A-исчислении, используемом для построения формальных семантик программ) Другая область, в которой понятие конечной итерации играет ключевую роль и в которой логическое моделирование является одним из основных методов исследования—это изучение знания в мульти-агентных системах, то есть в формальных моделях совокупности взаимодействующих познающих субъектов, в которых оператор конечная итерация используется для формального моделирования так называемого «общего знания», то есть знания о некотором факте, которое доступно всем познающим i

субъектам, наряду со знанием о самой этой доступности

Третья группа логик, рассматриваемых в настоящей диссертации,— это логики с экзистенциальной модальностью (#), называнной нами

так потому, что в семантике крипкевского типа формула р означает, что существует, некоторое (атомарное) отношение достижимости Иа такое, что формула уз истинна в точке, достижимой по Яа Эта модальность совсем недавно привлекла внимание логиков-прикладников в контексте логического моделирования полуструктурированньгх данных Полуструктурированными называют данные, которые имеют определенную структуру, но не настолько строгую, как базы данных; мотивирующий пример полуструктурированных данных—сеть Интернет Полуструктурированные данные обычно моделируются при помощи графов с отмеченными ребрами (то есть графов, в которых не только узлы, но и ребра имеют имена) Для рассуждения о полуструктурированных данных в литературе был предложен широкий круг формальных языков. Многие из этих языков оказались вариантами модальных языков (что неудивительно, поскольку графы могут быть естественным образом рассмотрены как крипкевские модели) В частности, Н Алешиной, С Демри и М де Райке для рассуждений о полуструктурированных была предложена модальная логика Р01_1"11'1 Модальность {#), одна из модальностей языка РОЦт'к, естественным образом возникает в контексте полуструктурированных данных (например, рассуждая о сети Интернет, мы часто хотим иметь возможность сказать в используемом нами формальном языке, что какая-то интернет-страница достижима из другой интернет-страницы по какой-то ссылке, и нам не важно, как эты ссылка обозначена на ссылающейся странице)

означают, что доказательство любых достаточно общих результатов об интуиционистских модальных логиках является довольно-таки затруднительным В частности, нелегко сформулировать достаточно общий метод доказательства разрешимости интуиционистских модальных логик До настоящею времени единственный метод обоснования разрешимости интуиционистских модальных логик, предложенный в литературе,—это погружение интуиционистских модальных логик с п модальностями в классические модальные логики (называемые классическими «напарниками» интуиционистских логик) с п + 1 модальностями, предложенное Ф Вольтером и М Захарьящевым Метод Вольтера и Захарьящева имеет строгое ограничение- он может быть использован для обоснования разрешимости только тех интуиционистских логик, разрешимость чьих классических напарников нам уже известна Общих методов доказательства разрешимости интуиционистских модальных логик, не зависящих от известности нам разрешимости их классических напарников, в литературе предложено не было

Что касается второго класса логик, исследуемых в диссертации, класса расширений минимальной нормальной логики с оператором €> , следует заметить, что несмотря на то, что сам оператор О давно известен (он был введен в 1970-х годах В. Праттом) и аксиоматически охарактеризован (К. Сегербергом), исследованием класса расширений минимальной нормальной логики с О до настоящего времени никто не занимался

Что касается логик с экзистенциальной модальностью (#), то модальность (#) привлекла внимание логиков совсем недавно, и к настоящему времени единственной работой, посвященной логикам с {М), является статья Н Алешиной, С Демри и М де Райке, в которой семантически определяется и изучается логика РОи*"'1. Важно отметить, что для практических применений РЭ1для которых она была предложена (рассуждения о полуструктурированных данных), существенно важно наличие дедуктивной системы, позволяющей обосновать те (и только те) выоды, которые законны в РОУ*"1, однако, в настоящее время работы, посвященные аксиоматизации Р01_'*"л, в

литературе отсутствуют

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

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

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

• Построение непротиворечивой и полной аксиоматизации логики р¡3и ряда связанных с ней логик.

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

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

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

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

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

• Доказано обобщение результата Ганиингера, Мейера и Вине-са о разрешимости двух-переменного монадигческого гардидного фрагмента перзопорядковой логики (' с условиями замкнутости, выразимыми в монадической второпорядковой логике, наложенными на отношения, обозначенные предикатными параметрами „„-формул, на фрагмент, в котором на отношения, обозначенные предикатными параметрами С/^т-формул, может быть наложено более одного условия

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

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

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

• Доказано, что добавление аксиом, характеризующих О , к логике й4 дает систему, эквивалентную Э4

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

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

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

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

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

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

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

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

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

• Доказано обобщение результата Ганцингера, Мейера и Вине-са о разрешимости двух-переменного монадического гардидного фрагмента первопорядковой логики GF^ с условиями замкнутости, выразимыми в монадической второпорядковой логике, наложенными на отношения, обозначенные предикатными параметрами CFj^-формул, на фрагмент, в котором на отношения, обозначенные предикатными параметрами СГ'?аоп-формул, может быть наложено более одного условия

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

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

• Построены аксиоматизации гильбертовского типа минимальной нормальной логики с экзистенциальной модальностью {#), ее детерминистичекого расширения, логики Р01'""к и одного из ее вариантов; доказана их семантическая адекватность и полнота

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

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

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

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

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

Апробация работы. Результаты диссертационного исследования были представлены на конференции «Methoda for Modalities 4», проводившейся в Нанси в 2004 г

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

Основное содержание работы

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

Первая глава диссертации называется «Модальная логика и гардидные фрагменты» Это глава, состоящяя из четырех разделов, содержит сведения о пропозициональных модальных логиках и гардидных фрагментах логик первого и более высоких порядков, на которые мы опираемся в последующих главах диссертации.

В первом разделе—*Модальная логика и первопорядковая логика» —дается определение пропозициональных моно- и полимодальных логик и классической первопорядковой логики

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

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

представляют собой реляционные структуры Ван Бентемом был сфор мулирован так называемый «стандартный период», отобравжающий модальные формулы в первопорядковые, что показало, что первопо-рядковьтй язык является не беднее пропозиционального модального языка

Определение 1. Пусть М С - это пропозициональный модальный язык и '£0—это псрвопорядковый язык Определим, при помощи взаимной индукции дер функции, г, и Ту отображающие формулы МС в формулы ТО тх определяется следующими условиями

• Тх(Рг) = Л(^) ДОЯ каждого р.,

• тх(ц>\/1р) Тх(ф) V тх(тр),

• тх(Оф) — Эу(й(х у)Лту{ч>))

ту определяется аналогично, с заменой х на у и у на г Наконец, будем называть стандартным переводом формулы уз е МС формулу тт(^>)

Ван Бентемом, в соавторстве с Немети и Андрекой, также было доказано, что первопорядковые переводы модальных формул («модальный фрагмент первопорядковой логики») являются собственным подмножеством множества первопорядковых формул

В третьем разделе— «Первопорядковые гардидные логики» описываются гардидные фрагменты первопорядковой логики

Гардидные фрагменты возникли в результате попытки получить более богатые, чем модальный фрагмент, фрагменты первопорядковой логики, сохраняющие «хорошие свойства» модального фрагмента, прежде всего разрешимость Базисный гардидный фрагмент обобщает «модальную квантификацию», то есть квантификацию, допутимую в модальном фрагменте: Э(/(Я(х,у) л т„(^)) Формулы базисного гардидного фрагмента строятся из атомарных формул при помощи булевых связок и квантификации следующего вида: если р—это атом, уз—формула гардидного фрагмента, и 7 С П/(<р) с РУ(р), то

37(р Л /) тоже является формулой гардидного фрагмента (г обозначает упорядоченную последовательность индивидных переменных, и /' 1<'(»') обозначает множество свободных переменных формулы формула р называется гардом формулы =1х(р Л (/?))

В разделе строится альтернативная семантика базисного гардидного фрагмента при помощи моделей с органиченным множеством допустимых приписываний и доказывается, что построенная семантика адекватна стандартной первопорядковой семантике гардкдньгх формул в том смысле, что всякая гардидная формула <р общезначима в классе альтернативных моделей, если и только если она общезначима в классе стандартных первопорядковых моделей Также в разделе приводится теоретико-модельное доказательство разрешимости базисного гардидного фрагмента, которое является аналогом алгебраического доказательства ван Вентема, Андреки и Немети Раздел равершается обзором более богатых, чем базисный гардидный фрагмент, гардидных фрагментов первопорядковой логики

В четвертом разделе— «Гардидные логики более высоких порядков логики»—описываются гардидные фрагменты логик более высоких порядков

Основное внимание в разделе уделяется гардидному фрагменту логики с оператором наименьшей неподвижной точки, исследованной в работах Э Грэделя и И Валукевича В частности, приводится полученный этими авторами результат о разрешимости гардидного фрагмента с оператором наименьшей неподвижной точки

Во второй главе— «Интуиционистские модальные логики»— описывается построенный нами общий метод доказательства разрешимости интуиционистских модальных логик через погружение в разрешимый гардидный фрагмент классической первопорядковой логики Глава состоит из семи разделов

В первом разделе обосновыется необходимость построения нового общего метода доказательства разрешимости интуиционистских модальных логик Указывается, что единственный общий метод доказательства разрешимости этих логик, предложенный Ф Вольтером и М В Захарьящевый, обладает очень важным ограничением- обосно-

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

Во втором разделе мы определяем двух-переменный монадический гардидный фрагмент первопорядковой логики

Определение 2. Двух-переменныч монадическим гардидным фрагментом (У/^Доп первопорядковой логики будем называть наименьшее подмножество гардидного фрагмента первопорядковой логики содержащее формулы у? гакие, что (¡) имеет не более двух переменных (свободных или связанных), и (л) все не-унарные предикатные параметры ¡р встречаются в гардах

В третьем разделе мы определяем условия замкнутости, которые могут накладываться на предикатные параметры формул без

потери разрешимости

Определение 3. Пусть И7—непустое множество Будем называть унарную ф>нкцию С на 2й' просхым ииераюром замыкания, если для всех V, V С IV имеют место следующие условия.

1 V С С (Г) (С растет),

2 V С Р' влечет С(Т) С С(Т") (С монотонен)

3 С('Р) = С (С (Г)) (С идемпотентен)

Будем называть п +- 1-местную функцию С на 2™ параметризованным оператором замыкания, если С(Ть ~Рп,—) является простым опера тором замыкания для любых Т\, , Тп с № Мы будем обозначать при

помощи С- т' операторы замыкания парамегризовашшр отношениями Т>1 , Рп

Определение 4. Будем называть условие наложенное на отношение Р, простым угловирм ¡амкнуто<ти, если оно может быть выражено в виде С(Р) — V где С простой оператор замыкания

Б\дем назыкахь условие наложенное на отношение V, параметризованным условием замкнутости если оно может быть кыражрно в виде (У* т (р) — р, где С^1' '''"—параметризованный оператор замыкания

Определение 5. Пусть 5 конечное множество отношений, С—множество условий замкнутости наложенных на эти отношения и С(Т)—все условия замкнутости из С, наложенные па отношение V из 6' Будем на^ывахь С ацикличным, если имеется такое упорядочивание Т>\ Рп множества ? чю С(#Рг+]) не имеет параметров, отличных от Р\ ,Р,

Определение 6. Будем иазьш&гь оператор замыкания Ср1 р" на п-местных отношениях тзо-определимым, если существует монадичегкая второпорядковая формула Ср' р", содержащая предикатные парамет ры Рь , Рт и Р, такая, что для любой модели М и любой п-местной формулы (то есть, формулы с п свободными переменными) ¡р имеет место __

сп = 'р-ЫР))\\м

Раздел завершается доказательством того, что двух-переменный монадический гардидный фрагмент Сна предикатные параметры которого наложено ациклическое множество шзо-определимых условий замкнутости, разрешим

Теорема 1. Пусть ^ £ и С—ацикличное множесхво тбо-

определичых условий замкнутости, наложенных на отношения из <р, хакое, что на каждое отношением наложено не более одного условия замкнутости Проблема выполнимости <р в модели, удовлетворяющей все условия из С, разрешима

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

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

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

Теорема 2. Пусть М—класс интуициони<лских модальных моделей, определенных при иомощи ацикличною множества гто-определимых условий з&мкнумсти, наложенных на Т1 Иа и 7?<>, таким образом чю не более чем одно условие замкнутости соответствует каждому из Э1их отношений, и пусть </?—это интуиционистская модальная формула Тогда, проблема выполнимости увМ разрешима

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

В третьей главе— «Логики с оператором Сегерберга»— исследуется решетка логик, содержащих два модальных оператора' обычный оператор возможности О и оператор конечной итерации, или оператор Сегерберга, <£> Глава состоит из пяти разделов

В первом разделе обосновывается актуальность исследования логик с оператором Сегерберга. Указывается, что такое исследование является естественным развитием предыдущих исследований в области модальных логик

Во втором разделе определяется язык исследуемых в главе логик и формулируется его семантика.

В третьем разделе приводся сведения о нормальных модальных

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

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

Определение 7 Seg = К* (О {П<£ «-» -р Л D3/- уз Л С% Dip) -» И^}

Также доказывается, что логика Seg имеет конечные нестандартные модели

В пятом разделе доказывается ряд результатов, проясняющих конфигурацию решетки расширений Seg

Теорема 3. Пусть Л- нормальная модальная логики в мономодалыюм языке MC и пусть Л* — \ ф Seg Тогда, Л* явтяется консервативным расширением Л

Теорема 4. Seg в S4 - S4 ф П^ «-> Ор

Теорема 5 (Аналог теоремы Макинсона). Пусть Л—это непротиворечивое расширение Seg Тогда, или Л С fCrrtf или Л С к™*

В четвертой главе - «Логики с экзистенциальной модальностью»—строятся аксиоматизации и доказывается полнота ряда логик, языки которых содержат модальный оператор {#), имеющий следующее условие истинности в крипкевских моделях- — (Jl6/72.,, где )JlSi7£, является объединением всех атомарных отношений достижимости модели Глава состоит из двух разделов.

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

(АО) Все классические тавтологии,

(К) [ir\(v V)([K)v{-пЩ,

(ЕЙ) 1г)р -{#)<р

Правила вывода:

(МР) Из 1р —» ф и ¡р можно вывести (N) Из р можно вывести

(ЕЬ) Из {г)<р ■» у можно вывести -> V, при условии что г не

встречается в

Также строится аксиоматизация детерминистического расширения К^, которое мы называем Г)К# Аксиоматизация ГЗК^ получается из приведенной выше аксиоматизации К.. добавлением схемы аксиом

(Р) <0 ч> - [']■/>

Доказываются следующие теоремы

Теорема 6. К# непротиворечива и слабо полна по отношению к классу всех С Ц -шкал

Теорема 7. ОК# непротиворечива и слабо полна по отношению к классу детерминистических £#-шкал

В втором разделе строится аксиоматизация логики Р01_'и"', которая представляет собой расширение хорошо известной логики р01_ при помощи оператора обращения, оператора (#), модальной константы тождества гй и номинала (пропозиционального параметра, истинного в точности в одной точке крицкевской модели) г Схемы аксиом Р01_ро"' логично разделить на четыре части Первая часть описывает поведение пропозициональных связок и стандартных модальных операторов

(тг) И [ж] .

(АО) Все классические тавтологии,

(К) М (у»-» ([74 V?-» [т] V); (А1) (ж) ф <-» —■ [" 7Г ] «р

Вторая часть описывает свойства сложных модальных операторов'

(А2) <7Г1 О тг2) р ^ (т.\) (тг2) А (АЗ) <7Г! и Л-?) V < -> (п) р V (п2) (А4) (тг-)^. > V (тг) (тг*) у; (А5) >[тг]уз)->(у>

(А6) —> [ 7Г | (л") (А7) [ гг ] <тг> ч?, (А8) ^ ♦-» {х<1)<р, (Ей) (,)р (ф)<р

Третья часть описывает свойства номинала г (для этой цели в язык вводится модальный оператор ''-х,, известный из области гибридных логик)'

(А9) &г(у> - ('Э^ —

(А10) @г<)5 <-> (АН) гЛу — (А12)

(А13) <7г)@г^

Наконец, нижеследующая аксиома соответствует условию связанности шкал, на которых интерпретируется Р01ра'н (условие требующее, что для любых ы и е IV, существует последовательность точек ,и„

такая, что (1) ю — иь (2) о = ап, и (3) для всякого 1 < г «С п — 1, имеет место следующее или, для некоторого < Р или, для

некоторого г 6 /, и1+1Т1гщ)

(А14) ((# и #)*}г

Правила вывода рои**"1 (МР) Из <р —» ф и 1р вьшодима ф\ (N) Из ^ выводима [ттV. (NN) Из р выводима @г<р,

(ЕЬ) Из (г)р —г V выводима (^)р —> V, при условии, что < не встречается в Ф

Доказыватся следующие теоремы

Теорема 8. РОи*1"1 непротиворечива и слабо полна по отношению к классу всех Рй^^-шкал

Теорема 9. Р01_ра"1 без аксиомы (А14) непротиворечива и слабо полна по отношению к классу всех не обязательно связанных РО^'^-шкал

Также в разделе определяется перевод формул РО^'""' в гардидный фрагмент логики с оператором неподвижной точки Мы добавляем к языку РГЛ1*1"' бесконечное множество пропозициональных параметров А"! Х„ (мы называем такой расширенный язык £х(Р01 р0"1)) и определяем перевод для формул

Определение 8. Определим при помощи взаимной индукции, два семейства переводов {т"}„ьч и отображающие формулы языка

в формулы языка с оператором наименьшей неподвижной точки РО(ЬРР) т™ определяется следующими равенствами

. г» - Р(х),

. т;(х,) = Х,(х),

. т^ /ф)

• 7"((г)1р) -31/(П(аг 1, у) Л г^(уг)), для каждого

. т?{Щ<р) =dz3y(R(z X v)Ar>)

• т'х'<(i)<p) — dy(R(a, у x) Л Tytfi), для каждою г,

. /?((#)/>) = dzdy(rt(z у ijAijW,

• iliTlOT!) »>) =Г?((ТГ1) (7T2)VJ),

• ^'((^l ь ' уз) = ^((n) V) V т^1кг) ip),

. r? «**> p) = \LFP Xn v т« '(V V W Xn)](r)

г™ определяется аналогично, заменой г на p pa i в предше( гвующих равенствах Наконец будем называть стандартным переводом PDLpa"'-формулы tp формулу тх(р)

Сформулированный перевод дает нам следующую теорему

Теорема 10. PDL^"1 и все ее расширения, определимые семантически при помощи //GF-формул разрешимы

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

Результаты диссертационной рабо(ы нашли отражение в следующих публикациях автора:

[1] Alechzna N, Shkatov D On mtuitionistic modal logics // Proceedings of «Methonds for modalities 4» Nanci, 2004

[2] Шкатпов Д П. Аналог теоремы Макинсона для нормальных модальных логик с оператором Сегерберга // Логические исследования, №11. М , «Наука», 2004

[3] Alechma. N, Shkatov D A general method for proving decidability of mtuitionistic modal logics // Journal of Applied Logic, 2005

[4] Алешина H A , Шкатпов Д П О модальных логиках с экзистенциальной модальностью // Логическик исследования, №12 М., «Наука», 2005

Шкатов Дмитрий Петрович

Автореферат диссертации на соискание ученой степени кандидата филосовских наук

Подписано в печать 2 05 2006 г Формат 60x90, 1 /16 Объем 1,5 п л Гираж 100 экз Заказ № 520

Отпечатано в ООО "Фирма Блок" 107140, г Москва, ул Краснопрудная, вл 13 т 264-30-73 www.blok01centre.narod.ru Изготовление брошюр, авторефератов, печать и переплет диссертации

«2106 13

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

Введение

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 без связанности

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

Актуальность темы. Хотя модальная логика—это давно появившаяся и к настоящему времени достаточно хорошо развитая область исследований и "стандартные" модальные логики были тщательно изучены (в чем можно убедиться, пролистав фундаментальную монографию [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 шкалами, где все атомарные отношения достижимости должны быть детерминистическими.

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

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.