Топологические модальные логики с модальностью неравенства

Кудинов, Андрей Валерьевич

Топологические модальные логики с модальностью неравенства тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Кудинов, Андрей Валерьевич АВТОР

кандидата физико-математических наук УЧЕНАЯ СТЕПЕНЬ

Москва МЕСТО ЗАЩИТЫ

2008 ГОД ЗАЩИТЫ

01.01.06 КОД ВАК РФ

Диссертация по математике на тему «Топологические модальные логики с модальностью неравенства»

Автореферат диссертации на тему "Топологические модальные логики с модальностью неравенства"

Московский Государственный Университет имени М. В. Ломоносова

Механико-математический факультет

На правах рукописи УДК 510.643

КУДИНОВ Андрей Валерьевич

Топологические модальные логики с модальностью неравенства

01.01.06- математическая логика, алгебра, теория чисел

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Москва 2008

003454022

Работа выполнена на кафедре математической логики и теории алгоритмов Механико-математического факультета Московского государственного университета имени М.В. Ломоносова.

Научный руководитель: Официальные оппоненты:

Ведущая организация:

доктор физико-математических наук, профессор В. Б. Шехтман.

доктор физико-математических наук,

профессор А. В. Чагров

(Тверской государственный университет);

кандидат физико-математических наук, Р. Э. Яворский

(Математический институт им. В. А. Стеклова Российской академии наук).

Институт математики им. С. Л. Соболева Сибирского отделения РАН.

Защита диссертации состоится 5 декабря 2008 года в 16 часов 40 минут на заседании диссертационного совета Д.501.001.84 при Московском государственном университете имени М. В. Ломоносова по адресу: Российская Федерация, 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, 14 этаж)

Автореферат разослан 5 ноября 2008 года.

Учёный секретарь диссертационного совета Д.501.001.84 при МГУ, доктор физ-мат. наук, профессор

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

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

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

Как раздел математической логики, модальная логика появилась в начале XX века (в работах К. Льюиса, К. Гёделя и др.). В настоящее время модальная логика активно развивается, благодаря разнообразным применениям — в том числе, в информатике, математической лингвистике и основаниях математики. Основное отличие модальной логики от классической — использование дополнительных связок («модальностей»), таких как «необходимо», «возможно» и др.

В топологических моделях можно интерпретировать модальность □ («необходимо») как канторовскую операцию внутренности, а двойственную к ней модальность О («возможно») —как операцию замыкания. Основы для такой интерпретации были заложены К. Куратовским, который предложил определение топологического пространства с помощью операции замыкания. Аксиомы Ку-ратовского соответствуют аксиомам хорошо известной модальной логики S4. Более того, как показали Дж. Маккинси и А. Тарский1, логика S4 полна в топологической семантике.

В конце XX века была установлена связь между топологической семантикой модальных логик и задачами представления графической и пространственной информации, возникшими в теоретической информатике и информационных технологиях. В частности, для описания взаимного расположения пространственных объектов было предложено;2 исчисление RCC8, использующее 8 основных отношений между регулярными областями в топологическом пространстве. Как вскоре выяснилось3, это исчисление вкладывается в модальную логику S4U (S4 с универсальной модальностью). В настоящее время RCC8 и аналогичные исчисления применяются в географических информационных система^ (ГИС)

С.С. McKinsey, A. Tarski. The algctra of topology Annals of Mathematics, v.45(1944), 141-191.

2D A Randell, Z Cm and A. G. Cohn. A spatial logic based on regions and connections. In Principles of Knowledge Representation and Reasoning: Proceedings of the 3rd International Conference, pp. 165-176. Morgan Kaufmann, 1992.

3B. Bennett. Spatial reasoning with prepositional logic. In. Proceedings of the 4th International > Conference on Knowledge Representation and Reasoning, pp. 51-62. Morgan Kaufmann, 1994.

4Smith, T. and Park, K. An algebraic approach to spatial reasoning. International Journal of

и других областях информатики.

Топологическая семантика □ может быть сформулирована эквивалентным образом: каждая пропозициональная формула интерпретируется как подмножество топологического пространства («множество точек, где формула считается истинной»). Тогда формула Оф истинна в точке х, если ф истинна в некоторой окрестности х.

Начиная с конца 1950-х годов для модальной логики получила широкое распространение реляционная семантика Крипке, основанная на сходной идее. При этом формулы интерпретируются в реляционных структурах («шкалах Крипке»), а формула Пф истинна в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению. Отметим, что для расширений логики54 реляционная семантика является частным случаем топологической семантики: шкалы Крипке в точности соответствуют так называемым «александровским пространствам», в которых любое пересечение открытых множеств открыто.

Всевозможные расширения логики Б4 описывают разнообразные свойства топологических пространств и шкал Крипке Однако далеко не все свойства топологических пространств выразимы модальными формулами в стандартном языке с модальностью □. Так, в работе Дж. Маккинси и А. Тарского (1944) доказано, что в стандартной топологической семантике логика Б4 полна относительно любого сепарабельного плотного в себе метрического пространства. Отсюда следует, что в этом языке невыразимы связность, компактность и многие другие свойства. Однако выразимость модального языка можно увеличить с помощью дополнительных модальностей. Приведем некоторые примеры.

Деривационная модальность □ в топологической модели интерпретируется следующим образом: Ц\ф истинно в точке х, если ф истинно в некоторой проколотой окрестности х. (Модальность □ выражается через □ Оф □ ф А ф) При такой интерпретации двойственная модальность 0 соответствует канторов-ской операции взятия производного множества (множества предельных точек). Первоначальное изучение модальности □ было начато также в работе Дж. Маккинси и А. Тарского (1944). Логики с деривационной модальностью подробно

Сео^арЫса! МогтаЬоп Бу^етз, 6:177-192, 1992.

исследовались в работах5'6'7, где был получен ряд результатов о полноте и выразимости. С помощью модальности □ удается выразить такие свойства, как плотность в себе и аксиому отделимости Т\.

Универсальная модальность [V] интерпретируется следующим образом: формула [V] ф истинна, если ф истинна во всех точках. При добавлении модальности [V] можно выразить новые топологические свойства, как, например, связность8.

Модальность неравенства изучению которой посвящена данная диссертация, интерпретируется следующим образом: формула [=истинна, если ф истинна во вссх точках, кроме, быть может, данной. Эта модальность впервые введена К. Сегербергом9 и исследована позднее рядом авторов (см. например10). (Отметим, что [V] выражается через \ф]: [V] <¿ \ф]ф Л ф.) Как было замечено11'12, при добавлении модальности становятся выразимыми многие свойства топологических пространств типа связности, плотности в себе и отделимости.

В гибридных модальных языках используется дополнительный сорт переменных (номиналы), причем в моделях номиналы должны быть истинны в единственной точке В недавней работе Т. Литака13 был исследован полиномиальный перевод из гибридной логики с универсальной модальностью в модальную логику с модальностью неравенства, и доказано, что он сохраняет выполнимость на классе топологических пространств.

Также отметим, что в настоящее время активно исследуются другие много-

5G. Bezhanishvili, L. Esakia, D. Gabelaia. Some results on modal axiomatization and definability for topological spaces Studia Lógica 81(3), pp 325-355, 2005.

6Л.Л Эсакиа Слабая транзитивность —реституция. Логические исследования, т8, стр 244245 Москва, Наука, 2001

7V Shehtman. Derived sets m Euclidean spaces and modal logic. ITLI Prepublication Senes, X-90-05, University of Amsterdam, 1990.

8V Shehtman. "Everywhere" and "Here". Journal of Applied Non-classical Logics, v.9 (1999), No 2/3, 369-380.

9K. Segerberg. A note on the logic of elsewhere Theoria, v. 46, No 2/3, pp 183-187, 1980.

l0V. Goranko Modal definability in enriched languages. Notre Dame, Journal of Formal Logic, No.l, pp. 81-105, 1989.

UB ten Cate, D Gabelaia, D. Sustretov. Modal languages for topology, expressivity and definability To appear in Annals of Pure and Applied Logic, 2008.

l2A. Kudinov. Topological modal logics with difference modality. In: Advances in Modal Logic, V.6, College Publications, London, 2006, 319-332.

13T. Litak. Isomorphism via translation. In: Advances in Modal Logic, V.6, College Publications, London,

2006, 333-351.

модальные логики, связанные с топологией: комбинированные пространственно-временные логики, динамические топологические логики, логики произведений топлогических пространств и логики метрических пространств (см Справочник по пространственным логикам14).

Цель работы

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

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

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

1) Найдены конечные аксиоматизации топологических модальных логик с модальностью неравенства для класса всех плотных в себе топологических пространств, для класса всех Т\-пространств и для класса всех плотных в себе Ti-пространств; доказана финитная аппроксимируемость и разрешимость этих логик.

2) Показано, что логика с модальностью неравенства пространства R" для n ^ 2 не зависит от п. Найдена конечная аксиоматизация этой логики, доказана финитная аппроксимируемость и разрешимость этой логики.

3) Доказана конечная неаксиоматизируемость топологических модальных логик с модальностью неравенства для прямой и окружности. Более того, доказана неаксиоматизируемость этих логик формулами с фиксированным конечным числом переменных.

Основные методы исследования

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

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

и Handbook of Spatial Logics. Editors: M. Aiello, I. Pratt-Hartmann, J van Benthem. Springer, 2007.

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

Для доказательства конечной неаксиоматизируемости логик прямой и окружности используются понятие «n-эквивалентности» на шкалах Крипке и характеристические формулы типа Янкова-Файна.

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

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

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

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

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

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

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

• на Международной конференции «Advances in. Modal Logic, 2006» (Нуза, Австралия, 2006),

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

• на международной конференции «Алгебраические и топологические методы в неклассических логиках III» (Оксфорд, Великобритания, 2007).

Публикации

Результаты автора по теме диссертации опубликованы в 4 работах, список которых приводится в конце автореферата.

Структура и объем диссертации

Диссертация состоит из введения, четырех глав, двух приложений и библиографии (40 наименований). Общий объем диссертации составляет 92 страница.

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

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

Фиксируем счетное множество пропозициональных переменных prop. Для натурального п ^ 1 п-модалъные формулы строятся рекурсивно с помощью множества Prop, константы «ложь» (±), импликации (—>) и п одноместных модальностей (dj, 02, ..., □„).

Двойственные модальности Ol определяются следующим образом: = -п^ф.

Множество всех п-модальных формул называется тг-модальным языком и обозначается M.£(0lt 02,..., □„).

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

Di(p я) —>• (niP —► Для всех г = 1,..., п;

и замкнутое относительно правил подстановки, Modus Ponens, введение модальности:

Пусть даны n-модальная логика L и множество формул Г, тогда через L + T мы будем обозначать минимальную n-модальную логику содержащую L U Г.

В диссертации рассматриваются только 1-модальные и 2-модальные логики. При этом □, О, [ф] и (ф) соответственно обозначают Oi, Oj, 02 и 02.

Определение 1. Фиксируем порядок пропозициональных переменных. Модальная формула называется т-формулой, если в ней встречается не более т первых переменных. Логика L называется т-аксиоматизируемой, если её можно аксиоматизировать с помощью т-формул.

Введем обозначение [V] ф [ф]ф А ф.

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

(BD) р->М&)р (45)

(Tu) Пр-»р

(40) Ор -> Odp

(Da) ¡V]p - аР

(AT,) ИР-И Qp

(DS) [ф]р -» Ор

(AC) [V] (Dp V СЬр) Мр V [V]-.р

(АЕк) ЩрА -пр А п(р -VÍ=i aQf) - víi1 а(р - -<9Í).

где для данного к формулы Q* (г = 1... к + 1) определяются следующим образом:

«-1 к = Q? = Д 9j A (для 1 < i < к), Qk+i = Д 9r j=i J=I

Рассматриваются следующие логики:

S4 = KX + ÍTo^D}, S4D = К2 + {То,4О,ВД,43,£>п}, S4DS = S4D + DS, S4DTi = S4D + ATi, S4DTiS = S4DTi + DS, Lk = S4DTiS + AE)¡, LCk = Lk + AC.

Определение 2. Пусть топологическое пространство. Топологической моделью на X называется пара (X, в), где функция в : PROP —* V(X) (оценка) сопоставляет каждой пропозициональной переменной р € PROP множество в(р) С X. Истинность формулы ф в точке х в топологической модели (X, в) (обозначение-

X, в, х ¡= ф) определяется по индукции:

Х,в,х\=р xee(j>),

Х,6,х\=ф->тр Х,в,х^ф клиХ,в,х\=ф,

Х,в,х\=Оф 3U(x)Vy 6 V(x) (X, в,у\=ф)

хе1{у\Х,в,У)гФ},

Определение 3. Формула ф общезначима в пространстве X, если она истинна в любой точке любой модели на X (обозначение: X (= ф).

Определение 4. Топологической модальной логикой с модальностью неравенства или D-логикой класса топологических пространств Т (обозначение: Ld{T)) называется множество всех формул языка МС{[=/]), общезначимых во всех пространствах класса Т. Логика L полка относительно Т, если Ld(T) = L.

Если X — топологическое пространство, то Ln({X}) сокращается до Ld(X).

Определение 5. Шкалой Крипке с п отношениями (или п-шкалой Крипке) называется кортеж F — {W, R\,..., Rn) такой, что я Rl<ZWxW для

всех г — 1,... ,п.

Определение 6. Моделью Крипке на шкале F = (W, R, Rd) называется пара М ~ (F, в), где 9 : PROP —> V{W) — оценка. Истинность формулы ф в точке х модели Крипке М определяется по индукции. Истинность атомарных формул и формул вида ф —> ф определяется, как в Определении 2, а истинность формул с модальностями — следующим образом:

М,х f= Оф Vy(xRy => М,у Н А)

М,х (= [ф\ф 4==$- Vy(xRDy => М, у (= ф) Определение 7. Формула ф общезначима в шкале F, если она истинна в любой точке любой модели на F (обозначение: F (= ф).

Определение 8. (Модальной) логикой класса шкал Крипке Т (обозначение: L{T)) называется множество всех формул, общезначимых во всех шкалах класса Т.

Для шкалы F мы пишем L(F) вместо L({F}).

Определение 9. Шкала Крипке ^ называется Ь-шкалой для модальной логики Ь, если Ь С Ь(Р).

Определение 10. Логика Ь называется полной относительно класса шкал С, если £(С) = Ь. Логика £ называется полной по Крипке, если она полна относительно некоторого класса шкал.

Определение 11. Пусть ^ = {У/, Я, До) — шкала Крипке, 5 = йи Яд, 5* — транзитивное и рефлексивное замыкание 5. Шкала Р называется конусом, если 5* (х) — V/ для некоторого х € IV

Хорошо известно, что любая полная по Крипке логика полна относительно некоторого класса конусов.

Известно, что логика Б40 полна относительно класса всех топологических пространств. Это следует из того, что она полна относительно всех шкал Крипке вида (V/, Я, 7^), где И транзитивко и рефлексивно.

В первой главе также доказывается полнота по Крипке всех рассматриваемых логик методом канонической модели.

Определение 12. Логика Ъ называется финитно аппроксимируемой, если она полна относительно некоторого класса конечных шкал.

теорема 13. Логики 5405, 540Т1, 540Т15, а также все логики [-к, 1Хк финитно аппроксимируемы.

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

СЛЕДСТВИЕ 14. Логики 540Б, 540Ть 540Тх5, а также все логики 1-к, 1-Ск разрешимы.

Это сразу следует из конечной аксиоматизируемости и финитной аппроксимируемости.

Во второй главе получены следующие результаты:

теорема 15. Логика Б405 полна относительно класса всех плотных в себе пространств.

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

теорема 16. б40т15 полна относительно произвольного нульмерного плотного в себе пространства.

Для доказательства полноты строится сохраняющее общезначимость отображение из нульмерного плотного в себе пространства на произвольный конечный 540Т]5-конуе.

следствие 17. 540т1б полна относительно класса всех плотных в себеТ\-пространств.

следствие 18. б40т1 полна относительно класса всех нульмерных пространств.

следствие 19. б40т1 полна относительно класса всех Т\-пространств.

В третьей главе изучаются Б-логики пространств Е", п > 2. Доказывается

теорема 20. Для любого логика 1_сх полна относительно к,".

План доказательства состоит в следующем. Сначала доказывается, что логика ЬСх полна относительного класса конечных шкал Крипке специального вида, которые называются аллеями. Затем доказывается, что для любой аллеи ^ существует отображение из И", где п ^ 2, на Г, сохраняющее общезначимость. Так как Е" |= 1_Сь то отсюда следует утверждение теоремы.

В четвертой главе изучаются Б-логики действительной прямой и окружности.

Включение Э 1-Сг легко проверяется. В действительности оказывает-

ся, что ¿о(Е) ф Юг и, более того, справедлива

теорема 21. В-логика прямой Ьц(е) не является п-аксиоматизируемой ни для какого п.

Доказательство проходит следующим образом. Для любого 1_Сг-конуса F мы определяем характеристический граф Г(Р), обладающий свойством: если существует отображение К —► сохраняющее общезначимость, то граф Г(Р) эйлеров15.

15Граф называется эйлеровым, если в нем существует путь проходящий по всем ребрам ровяо ло одному разу

Затем, аналогично работе16, мы строим две бесконечные последовательности -конусов (Рп)п>1 и такие что для любого п

(1) шкалы Рп и не различимы с помощью п-формул;

(2) граф Г(2?п) не эйлеров;

(3) существует отображение Ш, -+ сохраняющее общезначимость. Отсюда, используя характеристические формулы типа Янкова-Файна, мы получаем утверждение теоремы.

Аналогично, но с использованием несколько иной последовательности конечных шкал, доказывается

теорема 22. В-логика окружности не является п-аксиоматизируе-

мой ни для какого п.

В приложении А приведены оценки сложности логик, изучавшихся в диссертации.

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

Благодарности

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

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

Работы автора по теме диссертации

[1] A.B. Кудинов. О топологической модальной логике R с неравенством. Успехи математических наук, 2008, 63:1(379), 163-164.

[2] A. Kudinov. Topological modal logics with difference modality. Advances in Modal Logic, V.6. College Publications, London, 2006, 319-332.

[3] A Kudinov. Difference modality in topological spaces. In: Algebraic and Topological Methods in Non-classical Logics II, Barcelona, 2005, Abstracts, Universität de Barcelona, 50-51.

[4] A. Kudinov. Topological modal logic with the difference modality. In: Computer science applications of modal logic, Independent University of Moscow, September 5-9, 2005, Abstracts, 27-28.

Издательство ЦПИ при механико-математическом факультете МГУ имени М. В. Ломоносова

Подписано в печать ЗО. /О. О% Формат 60x90 1/16. Усл. печ. л. /¿> Тираж {РО экз. Заказ €И

Отпечатано с оригинал-макета на типографском оборудовании механико-математического факультета

Содержание диссертации автор исследовательской работы: кандидата физико-математических наук, Кудинов, Андрей Валерьевич

Введение

1 Обзор определений

1.1 Описание языка.

1.2 Аксиомы и логики.

1.3 Топологическая семантика.

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

1.5 Топологические пространства и шкалы Крипке с выделенными точками.

1.6 р-морфизмы.

1.7 Некоторые свойства топологических пространств с выделенными точками.

1.8 Свойства шкал Крипке.

1.9 Каноничность аксиом.

1.10 Фильтрация канонической модели.

2 Логики некоторых классов топологических пространств

2.1 Логики класса всех пространств и класса всех плотных в себе пространств.

2.2 Логики нульмерных и Ti-пространств.

3 Логика пространства Мп, для п ^

3.1 Аллеи.

3.2 Доказательство полноты.

4 Логики вещественной прямой и окружности 75 А Сложность изучавшихся логик 82 В Сводимость к гибридной логике

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

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

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

Как раздел математической логики, модальная логика появилась в начале XX века (в работах К. Льюиса [Lewis, 1918], К. Гёделя [Godel, 1933] и др.). В настоящее время модальная логика активно развивается, благодаря разнообразным применениям — в том числе, в информатике, математической лингвистике и основаниях математики. Основное отличие модальной логики от классической — использование дополнительных связок («модальностей»), таких как «необходимо», «возможно» и др.

В топологических моделях можно интерпретировать модальность □ («необходимо») как канторовскую операцию внутренности, а двойственную к ней модальность О («возможно») — как операцию замыкания. Основы для такой интерпретации были заложены К. Куратовским [Kuratowski, 1922], который предложил определение топологического пространства с помощью операции замыкания. Аксиомы Куратовского соответствуют аксиомам хорошо известной модальной логики S4. Более того, как показали Дж. Маккинси и А. Тарский [McKinsey, Tarski, 1944], логика S4 полна в топологической семантике.

В конце XX века была установлена связь между топологической семантикой модальных логик и задачами представления графической и пространственной информации, возникшими в теоретической информатике и информационных технологиях. В частности, для описания взаимного расположения пространственных объектов было предложено исчисление RCC8 [Randell et al., 1992], использующее 8 основных отношений между регулярными областями в топологическом пространстве. Как вскоре выяснилось [Bennett, 1994], это исчисление вкладывается в модальную логику S4U (S4 с универсальной модальностью). В настоящее время RCC8 и аналогичные исчисления применяются в географических информационных системах (ГИС) [Smith, Park, 1992] и других областях информатики.

Топологическая семантика для связки □ может быть сформулирована эквивалентным образом: каждая пропозициональная формула интерпретируется как подмножество топологического пространства («множество точек, где формула считается истинной»). Тогда формула Пф истинна в точке х, если ф истинна в некоторой окрестности х.

Начиная с конца 1950-х годов для модальной логики получила широкое распространение реляционная семантика Крипке, основанная на сходной идее [Kripke, 1959]. При этом формулы интерпретируются в реляционных структурах («шкалах Крипке»), а формула пф истинна в точке х, если ф истинна во всех точках, связанных с х по данному бинарному отношению. Отметим, что для расширений логики S4 реляционная семантика является частным случаем топологической семантики: шкалы Крипке в точности соответствуют так называемым «александровским пространствам», в которых любое пересечение открытых множеств открыто.

Всевозможные расширения логики S4 описывают разнообразные свойства топологических пространств и шкал Крипке. Однако далеко не все свойства топологических пространств выразимы модальными формулами в стандартном языке с модальностью □. Так, в работе [McKinsey, Tarski,

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

Деривационная модальность □ в топологической модели интерпретируется следующим образом: Е\ф истинно в точке х, если ф истинно в некоторой. проколотой окрестности х. (Модальность □ выражается через □: иф <£ф> Ц]ф а ф.) При такой интерпретации двойственная модальность 0 соответствует канторовской операции взятия производного множества (множества предельных точек). Первоначальное изучение модальности □ было начато также в работе [McKinsey, Tarski, 1944]. Логики с деривационной модальностью подробно исследовались в работах [Bezhanishvili et al., 2005], [Эсакиа, 2001], [Shehtman, 1990], где был получен ряд результатов о полноте и выразимости. С помощью модальности □ удается выразить такие свойства, как плотность в себе и аксиому отделимости Т\.

Модальность неравенства изучению которой посвящена данная диссертация, интерпретируется следующим образом: формула [у^]ф истинна, если ф истинна во всех точках, кроме, быть может, данной. Эта модальность впервые введена К- Сегербергом [Segerberg, 1980] и исследована позднее рядом авторов (см. например [Goranko, 1989], [de Rijke, 1992]). (Отметим, что [V] выражается через [уЦ: [V] ф [^}ф а ф.) Как было замечено в [ten Cate et al., 2008] и [Kudinov, 2006], при добавлении модальности [т^} становятся выразимыми многие свойства топологических пространств типа связности, плотности в себе и отделимости.

В гибридных модальных языках используется дополнительный сорт переменных (номиналы), причем в моделях номиналы должны быть истинны в единственной точке. В недавней работе [Litak, 2006] был исследован полиномиальный перевод из гибридной логики с универсальной модальностью в модальную логику с модальностью неравенства, и доказано, что он сохраняет выполнимость на классе топологических пространств.

Также отметим, что в настоящее время активно исследуются другие многомодальные логики, связанные с топологией: комбинированные пространственно-временные логики [Bennett et al., 2002; Kontchakov et al., 2007], динамические топологические логики [Kremer, Mints, 2005], логики произведений топлогических пространств [van Benthem et al., 2006] и логики метрических пространств [Konev et al., 2006; Sheremet et al., 2006]. Более подробно о современном состоянии в этой области см. [Aiello et al., 2007].

Цель работы

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

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

1) Найдены конечные аксиоматизации топологических модальных логик с модальностью неравенства для класса всех плотных в себе топологических пространств, для класса всех Ti-пространств и для класса всех плотных в себе Ti-пространств; доказана финитная аппроксимируемость и разрешимость этих логик.

2) Показано, что логика с модальностью неравенства пространства Rn для п ^ 2 не зависит от п. Найдена конечная аксиоматизация этой логики, доказана финитная аппроксимируемость и разрешимость этой логики.

Основные методы исследования

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

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

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

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

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

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

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

• на Международной конференции «Advances in Modal Logic, 2006» (Нуза, Австралия, 2006),

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

Публикации

Результаты автора по теме диссертации опубликованы в 4 работах: [Куди-нов, 2008], [Kudinov, 2006], [Kudinov, 2005а] и [Kudinov, 2005Ь].

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

Фиксируем счетное множество пропозициональных переменных Prop. Для натурального п > 1 п-модальные формулы строятся рекурсивно с помощью множества prop, константы «ложь» (l), импликации (—>) и п одноместных модальностей (Di, П2,., Пп).

Двойственные модальности О; определяются следующим образом: Oi</> = -.□ г^ф.

Множество всех n-модальных формул называется п-модальным языком и обозначается М£(пi, ., пп).

Пропозициональной п-модальной логикой называется множество п-модальных формул, содержащее все классические тавтологии, аксиомы нормалыюсти ni(p q) iPiV ni4), для всех г = 1,.,п; и замкнутое относительно правил подстановки (Sub), Modus Ponens (MP), введение модальности (—> Dj): для произвольной пропозициональной переменной р и г = 1,., п.

Пусть даны n-модальная логика L и множество формул Г, тогда через L + Г мы будем обозначать минимальную n-модальную логику содержащую LUT.

В диссертации рассматриваются только 1-модальные и 2-модальные логики. При этом □, О, у^] и соответственно обозначают Di, Оь П2 и 02.

Определение (1.1). Фиксируем порядок пропозициональных переменных. Модальная формула называется т-формулой, если в ней встречается не более га первых переменных. Логика L называется т-аксиоматизируемой, если её можно аксиоматизировать с помощью га-формул.

Введем обозначение [V] ф А ф.

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

Во)

45)

ЗЬ) Up —¥ р

4п) Пр □ Пр

АО MP

ATi)

DS) №Р оV

АС) [V](Dp V П-*р) [V]p V [V]->p

АЕк) &}р л —>р л п(р - VS - v-i1 - -Q?), где для данного к формулы Q^ {г = 1. к + 1) определяются следующим образом: i-l к Qi = -^ъ Qi = Д Яз л (для 1 < г ^ к), Qkk+1 = Д q5.

Рассматриваются следующие логики:

S4 = Ki + {Tn,4n}, S4D - К2 + {ТП,4 □ , Bp, D S4DS = S4D + DS, S4DTi = S4D + ATi, S4DTiS = S4DTi + DS, Lk = S4DTiS + AEk: LCk = Lk + AC.

Определение (1.8). Пусть X— топологическое пространство. Топологической моделью на X называется пара (£,0), где функция 9 : PROP —► V{X) (оценка) сопоставляет каждой пропозициональной переменной р G PROP множество в(р) С X. Истинность формулы ф в точке х в топологической модели (X, 0) (обозначение: Х,0,х |= ф) определяется по индукции:

Х:в:х\=р хЕв(р), Зс ^ ^ 00 ^

X, в, х (=</>—> ф Х:в,х Ф или Х,в,х (= ф,

Х,в,х\=Пф х <Е 1{у | Х,в,у |= 0},

Х,в,х\=&]ф Уу^х(Х,в,у^ф).

Определение (1.9). Формула ф общезначима в пространстве X, если она истинна в любой точке любой модели на X (обозначение: X \= ф).

Определение (1.10). Топологической модальной логикой с модальностью неравенства или D-логикой класса топологических пространств Т (обозначение: Ljr>(T)) называется множество всех формул языка Л4£(П, [у^]), общезначимых во всех пространствах класса Т. Логика L полна относительно Т, если Ad(T) = L.

Если X — топологическое пространство, то Ld({X}) сокращается до Ld(X).

Определение (1.15). Шкалой Крипке с п отношениями (или п-шкалой Крипке) называется кортеж F — (W, Ri,., Rn) такой, что W ф 0 и Ri С Ж х W для всех г = 1,., п.

Определение (1.17). Моделью Крипке на шкале F — (W, R, Rd) называется пара М = (F, где в : Prop —> V(W) — оценка. Истинность формулы ф в точке х модели Крипке М определяется по индукции. Истинность атомарных формул и формул вида ф —» 'ф определяется, как в Определении 1.8, а истинность формул с модальностями — следующим образом:

М,х\=Пф Vy{xRy => М,у \= А)

М, ж |= [ф]ф Vy(xRDy М, у \=ф)

Определение (1.18). Формула ф общезначима в шкале F, если она истинна в любой точке любой модели на F (обозначение: F [= ф).

Определение (1.20). (Модальной) логикой класса шкал Крипке Т (обозначение: Ь{Т)) называется множество всех формул, общезначимых во всех шкалах класса Т.

Для шкалы F мы пишем L(F) вместо L({F}).

Определение (1.21). Шкала Крипке F называется h-шкалой для модальной логики L, если L с L(F)-.

Определение (1.11). Логика L называется полной относительно класса шкал С, если L{C) = L. Логика L называется полной по Крипке, если она полна относительно некоторого класса шкал.

Определение (1.16). Пусть F = (W,R,Re>) — шкала Крипке, S = R U Rd, S* — транзитивное и рефлексивное замыкание S. Шкала F называется конусом, если S*(x) — W для некоторого х е W.

Хорошо известно, что любая полная по Крипке логика полна относительно некоторого класса конусов.

Известно также, что логика S4D полна относительно класса всех топологических пространств (см. [de Rijke, 1992]). Это следует из того, что она полна относительно всех шкал Крипке вида (W, R, ф), где R транзитивно и рефлексивно.

В первой главе также доказывается полнота по Крипке всех рассматриваемых логик методом канонической модели.

Определение (1.80). Логика L называется финитно аппроксимируемой, если она полна относительно некоторого класса конечных шкал.

Теорема (1.86). Логики S4DS, S4DTi, S4DTiS^ а также все логики Lk, LCk финитно аппроксимируемы.

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

Следствие (1.87). Логики S4DS, S4DTb S4DTiS, а также все логики Lb LCk разрешимы.

Это сразу следует из конечной аксиоматизируемости и финитной аппроксимируемости.

Во второй главе получены следующие результаты:

Теорема (2.5). Логика S4DS полна относительно класса всех плотных в себе пространств.

Для доказательства полноты строится сохраняющее общезначимость отображение из плотного в себе пространства на произвольный конечный S4DS-KOHyc.

Теорема (2.9). Логика S4DTiS полна относительно произвольного нульмерного плотного в себе метрического пространства.

Для доказательства полноты строится сохраняющее общезначимость отображение из нульмерного плотное в себе пространства на произвольный конечный S4DTiS-KOHyc.

Следствие (2.11). Логика S4DT]S полна относительно класса всех плотных в себе Ti-пространств.

Следствие (2.12). Логика S4DTi полна относительно класса всех нульмерных пространств.

Следствие (2.13). Логика S4DTi полна относительно класса всех Т\-пространств.

В третьей главе изучаются D-логики пространств BJ1, п ^ 2. Доказывается

Теорема (3.19). Для любого п ^ 2, логика LCi полна относительно

План доказательства состоит в следующем. Сначала доказывается, что логика LCi полна относительного класса конечных шкал Крипке специального вида, которые называются аллеями. Затем доказывается, что для любой аллеи F существует отображение из Rn, где п ^ 2, на F, сохраняющее общезначимость. Так как Rn |= LCi, то отсюда следует утверждение теоремы.

В четвертой главе изучаются D-логики действительной прямой и окружности.

Включение Ld(R) Э LC2 легко проверяется. В действительности оказывается, что Ld(R) ф- LC2 и, более того, справедлива теорема (4.2). D-логика прямой Ad(R) не является п-аксиоматизируемой ни для какого п.

Доказательство проходит следующим образом. Для любого ЬСг-конуса F мы определяем характеристический граф T(F), обладающий свойством: если существует отображение R —> F, сохраняющее общезначимость, то граф Г(F) эйлеров1.

Затем, аналогично работе [Максимова et al., 1979], мы строим две бесконечные последовательности ЬСг-конусов (Fn)n^i и (F^n^i, такие что для любого п

1) шкалы Fn и F^ не различимы с помощью п-формул;

2) граф r(F„) не эйлеров;

3) существует отображение R —> F,сохраняющее общезначимость.

Отсюда, используя характеристические формулы типа Янкова-Файна, мы получаем утверждение теоремы.

Аналогично, но с использованием несколько иной последовательности конечных шкал, доказывается теорема (4.12). D-логика окружности Ld{S1) не является п-аксио-матизируемой ни для какого п.

В приложении А приведены оценки сложности логик, изучавшихся в диссертации.

1 Граф называется эйлеровым, если в нем существует путь проходящий по всем ребрам ровно по одному разу.

Список источников диссертации и автореферата по математике, кандидата физико-математических наук, Кудинов, Андрей Валерьевич, Москва

1. Александров П. Введение в теорию множеств и общую топологию. —1. Москва, Наука, 1977.

2. Александров П., Пасынков Б. Введение в теорию размерности. — Москва,1. Наука, 1973.

3. Bennett В. Spatial reasoning with prepositional logics // Principlesof Knowledge Representation and Reasoning: Proceedings of the 4th 1.ternational Conference, Morgan Kaufmann, San Francisco.—. 1994.— pp. 51—62.

4. Bezhanishvili G., Esakia L., Gabelaia D. Some Results on Modal

5. Axiomatization and Definability for Topological Spaces// Studia Logica. —2005. — Vol. 81, no. 3. — pp. 325-355.

6. Blackburn P., de Rijke M., Venema Y. Modal Logic. — Cambridge University1. Press, 2002.

7. Chagrov A., Zakharyaschev M. Modal Logic. — Oxford University Press,1997. de Rijke M. The Modal Logic of Inequality // Journal of Symbolic Logic. — 1992. — Vol. 57, no. 2. — pp. 566-584.

8. Sheremet M., Tishkovsky D., Wolter F., Zakharyaschev M. From topology88 ь

9. СПИСОК ИСПОЛЬЗУЕМОЙ ЛИТЕРАТУРЫ 89to metric: modal logic and quantification in metric spaces // Advances in

10. Modal Logic, College Publications, London. — 2006. — pp. 429-448.

11. Godel К Eine Interpretation des Intuitionistischen- Aussagenkalkiils //

12. Ergebnisse Eines Mathematischen Kolloquiums. — 1933. — Vol. 4. —p. 39-40.

13. Goranko V. Modal definability in enriched languages // Notre Dame J.

14. Formal Logic. — 1989. — Vol. 31, No 1. — pp. 81-105.

15. Handbook of Spatial Logics / Ed. by M. Aiello, I. E. Pratt-Hartmann,

17. Kremer P., Mints G. Dynamic topological logic // Annals of Pure and

18. Applied Logic— 2005.— Vol. 131, Nos 1-3.— pp. 133—158.

19. Kripke S.A.K Completeness Theorem in Modal Logic// Journal of Symbolic1.gic— 1959. —Vol.24, No 1.—pp. 1—14.

20. Kudinov A. Difference modality in topological spaces // Algebraic and

21. Topological Methods in Non-classical Logics II, Abstracts, Universitat de

22. Barcelona. — Barcelona: 2005. — pp. 50—51.

23. Kudinov A. Topological modal logic with the difference modality // Computerscience applications of modal logic, Abstracts, Independent University of

24. Moscow. — Moscow: 2005. — pp. 27-28.

25. Kudinov A. Topological Modal Logics with Difference Modality // Advancesin Modal Logic, College Publications, London. — 2006. — pp. 319—332.

26. Kuratowski К Sur I'operation A de I'Analysis Situs // Fundamenta

27. Mathematicae. — 1922. — Vol. 3. — pp. 182-199.

28. СПИСОК ИСПОЛЬЗУЕМОЙ ЛИТЕРАТУРЫ 90

29. Кудинов А. В. О топологической модальной логике И с неравенством //

30. Успехи математических наук. — 2008. — Т. 63, № 1(379). — с. 163—164.

31. Куратовский К. Топология. Том 1. — Мир, Москва, 1966.1.wis I. A survey of symbolic logic. — University of California Press, 1. Berkeley, С A, 1918. 1.tak T. Isomorphism via translation // Advances in Modal Logic, College

32. Publications, London. — 2006. — pp. 333—351.

33. McKinsey J. C, Tarski A. The algebra of topology // Annals of

34. Mathematics.— 1944. — Vol.45, no. 1.— pp. 141-191.

35. Bennett В., Cohn A. G., Wolter F., Zakharyaschev M. Multi-Dimensional

36. Максимова Л. Л., Скворцов Д. П., Шехтман В. Б. Невозможность конечной аксиоматизации логики финитных задач Медведева // Доклады

37. АН СССР. — 1979. — Т. 245, № 5. — с. 1051-1054.

38. Konev В., Kontchakov R., Wolter F., Zakharyaschev M. On Dynamic

39. Topological and Metric Logics // Studia Logica.— 2006.— Vol. 84,no. L — p p . 129-160.

40. Randell D. A., Cui Z., Cohn A. G. A Spatial Logic based on Regionsand Connection // In Proceedings of the 3nd Conference on Knowledge

41. СПИСОК ИСПОЛЬЗУЕМОЙ ЛИТЕРА ТУРЫ Ш

42. Representation and Reasoning, Morgan Kaufman.— 1992.— pp. 165—176.

43. Reynolds M. The complexity of the temporal logic over the reals. — Submited,2008. http://www.esse.uwa.edu.au/mark/research/Online/CORT.htm.

44. Расева E., Сикорский P. Математика метаматематики. — Наука, Москва,1972.

45. Sahlqvist И. Completeness and correspondence in the first and second ordersemantics for modal logic // Proceedings of the Third Scandinavian Logic

46. Symposium, Amsterdam, North-Holland. — 1975. — pp. 110—143.

47. Segerberg К A note on the logic of elsewhere // Theoria. — 1980. — Vol. 46,no. 2/3.—pp. 183-187.

48. Shapirovsky /., Shehtman V. Modal Logics of Regions and Minkowski

49. Spacetime // Logic Computation. — 2005. — Vol. 15, no. 4. — pp. 559—574.

50. Shehtman V. Derived sets in Euclidean spaces and modal logic: Tech. rep.:

51. LI Prepublication Series, University of Amsterdam, X-1990-05, 1990.

52. Shehtman V. B. "Everywhere" and "here" // Journal of Applied Non

53. Classical Logics. — 1999. — Vol. 9, no. 2-3. — pp. 369-380.

54. Smith T. R., Park К К Algebraic approach to spatial reasoning //1.ternational Journal of Geographical Information Science. — 1992. —

56. Kontchakov R., Kurucz A., Wolter F., Zakharyaschev M. Spatial Logic +

57. Temporal Logic = ? // Handbook of Spatial Logics / Ed. by M. Aiello,

58. СПИСОК ИСПОЛЬЗУЕМОЙ ЛИТЕРАТУРЫ

59. Pratt-Hartmann, J. V. Benthem. — Springer Netherlands, 2007. —pp. 497-564.

60. Electronic Notes in Theoretical Computer Science. — 2007. — Vol. 174,no. 6. — pp. 79-94.

61. Эсакиа Л. Л. Слабая транзитивность — реституция // Логические исследования, — 2001. — Т. 8. — с. 244-245.