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

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

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

Введение

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], где был получен ряд результатов о полноте и выразимости. С помощью модальности □ удается выразить такие свойства, как плотность в себе и аксиому отделимости Т\.

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

Модальность неравенства изучению которой посвящена данная диссертация, интерпретируется следующим образом: формула [у^]ф истинна, если ф истинна во всех точках, кроме, быть может, данной. Эта модальность впервые введена К- Сегербергом [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 не зависит от п. Найдена конечная аксиоматизация этой логики, доказана финитная аппроксимируемость и разрешимость этой логики.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• на международной конференции «Алгебраические и топологические методы в неклассических логиках III» (Оксфорд, Великобритания, 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 Граф называется эйлеровым, если в нем существует путь проходящий по всем ребрам ровно по одному разу.

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

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.