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

• Мурзина, Вета Федоровна
• кандидат физико-математических наук
• 2003

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

Введение

1 Логики а-пространств

1.1 Основные понятия.

1.1.1 Топологические пространства Ершова.

1.1.2 Модальные логики и шкалы Крипке.

1.1.3 Канонические модели.

1.1.4 Финитно модельное свойство и фильтрации

1.2 Теорема о корректности.

1.3 Логические исчисления LD и I/.

1.4 Канонические модели для LD и I/.

1.5 Разрешимость исчислений LD, I/.

2 Модальная логика строго линейно упорядоченных /шкал

2.1 Постановка задачи.

2.2 Lf и структура канонической модели

2.3 Теорема о полноте

2.4 Финитная аппроксимируемость Lf.

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

3.1 Теорема о корректности.

3.2 Канонические модели для L*f и L*fo.

3.3 Теорема о полноте.

3.4 Финитная аппроксимируемость L*f, L*fo.

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

Теория неклассических логик - одна из важных областей современной логики. Особую роль играют модальные и временные логики. Хотя изучение логических свойств модальностей началось ещё во времена Аристотеля, теория модальных логик является сравнительно новым разделом математической логики: в начале 20-го века К.Льюис сформулировал первые модальные исчисления, а стремительный рост в этой области начался в 40-е - 50-е гг, благодаря работам С.Крипке, К.Льюиса, Дж.МакКинси, Б.Йонссона, А.Тарского и др. Временная логика, как независимая область исследования, возникла благодаря работам Прайора [23].

Модальная логика по сравнению с классической логикой, отличается большим разнообразием синтаксиса и семантики: кроме обычных логических связок используются различные модальности типа необходимости и возможности. Этим можно объяснить широкое применение модальных и временных логик, например, в информатике, теории искусственного интеллекта, математической лингвистике. Здесь можно упомянуть различные работы, связанные с методами представления знаний [31], [17], логикой стрелок [30]. Теория временных логик также является особенно важной в связи с развитием параллельных вычислений (см.,например, [22]).

В последнее время неклассические логики широко применяются к изучению геометрических структур (например, модальные логики подмножеств действительной плоскости [28], интервальные временные логики [9]) и топологических пространств. Так, например, в [8] В.Б. Шехтманом в языке с оператором локальной и универсальной истинности построена система аксиом и доказана финитная аппроксимируемость логики произвольного связного, плотного в себе сепарабельного метрического пространства. Также в [8] построена система аксиом для логики рациональной прямой и логики класса всех линейных порядков в языке с временными операторами и операторм локальной истинности.

Применение модальной логики к изучению топологических пространств можно объяснить тем, что модальные логики высказываний можно исследовать с точки зрения их топологической (окрестностной) семантики. Топологическая интерпретация модальности была дана в работах Дж. МакКинси и А.Тарского [21], где была доказана топологическая полнота широко известной модальной логики S4, и позднее в [24]. В окрестностной семантике "необходимость" (□) интерпретируется как "локальная истинность" [24]: если рассматривать точки топологического пространства X как возможные миры, в которых формулы истинны или ложны, то формула ПА истинна в х G X , если А истинна в некоторой окрестности мира х.

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

В данной работе исследуются полимодальные логики, связанные с топологическими пространствами Ершова («-пространствами, /пространствами, /о-пространствами). При этом рассматривается следующий вопрос: построение логики, описывающей данный класс топологических пространств, и исследование её свойств.

Понятие /-пространства было введено Ю.Л.Ершовым [2], [3], с целью развить теорию вычислимых функционалов. Кроме того, пространства Ершова можно рассматривать как топологический подход к теории областей Ершова-Скотта (domain theory), см. [13], которая является одним из важных разделов современной математики. Теория областей Ершова-Скотта возникла в 70-е гг. независимо в работах Ю.Л.Ершова ([12], [1]) и Д.Скотта [25]. Скоттом теория областей введена как теория программных языков и наиболее развилась в теоретической информатике. В [13] Ю.Л.Ершовым доказано, что введенное Д.Скоттом понятие 5-domain и понятие полного /о-пространства эквивалентны.

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

Реляционная семантика (или семантика Крипке) является основным инструментом в модальной логике. Реляционная семантика была введена неявно Б.Йонссоном и А.Тарским [29], Дамметтом и Леммоном [11], явно — в работах С.Крипке [18], [19], и использует понятие шкалы. Шкалой Крипке называется непустое множество (множество возможных миров) с заданным на нем бинарным отношением достижимости. Если (X, R) — шкала Крипке, то модальность □ можем связать с отношением R и понимать ее как истинность во всех достижимых мирах. Если мы рассматриваем временную логику, то с бинарным отношением R связываем две модальности: прошлого (□*) и будущего (□). Тогда в случае шкал Крипке определение истинности в точке (для формул вида □М, ПЛ) приобретает вид: я |= п*А <=> Vy(yRx у |= А), х\=ПА ■<==$■ My{xRy ==> у [= А).

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

Цель работы — найти модальные и временные логики, которые характеризуют классы шкал, основанных на пространствах Ершова.

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

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

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

1) Строятся полимодальные исчисления, корректные относительно шкал, основанных на си-пространствах. Доказывается разрешимость этих исчислений.

2) Введены классы строго линейно упорядоченных /-шкал и строго линейно упорядоченных /о-шкал. Найдено модальное исчисление, полное относительно этих классов. Доказано, что оно обладает финитно модельным свойством.

3) Построены два исчисления временной логики, одно из которых характеризует класс строго линейно упорядоченных /-шкал, другое — класс строго линейно упорядоченных /о-шкал. Доказана финитная аппроксимируемость этих исчислений.

Работа носит теоретический характер. Ее методы и результаты могут быть полезны специалистам в области неклассических логик Института Математики СО РАН, Московского, Новосибирского, Красноярского и др. госуниверситов.

Основные результаты, полученные в диссертации, докладывались на:

• заседаниях семинаров "Алгебра и логика" и "Нестандартные логики" кафедры алгебры и математической логики механико-математического факультета НГУ,

• международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибиск,1999),

• международной конференции "Мальцевские чтения" (Новосибирск, 2000),

• логическом коллоквиуме LC'03 (Хельсинки, 2003).

Результаты диссертации опубликованы в семи работах автора [32]

38].

Остановимся более подробно на содержании работы.

В главе 1 исследуются полимодальные логики на основе а- пространств Ершова.

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

В параграфе 1.2 вводится понятие окрестностной а-шкалы, связанное с понятием а-пространства. При этом рассматриваются пятерки вида (X, Хо, т, <, -<), где Хо С X, т — топология на X и <, -< — бинарные отношения на X.

Для шкал такого вида естественно рассматривать язык полимодальной логики с пятью модальностями: локальной истинностью определяемой топологией т, временными модальностями □<, □<, связанными с отношением <, и временными модальностями связанными с отношением Так как имеется выделенное подмножество, то в язык вводится дополнительная константа /3, которая описывает это подмножество.

В языке с модальностями □, □<,□<, Ш^, СЦ и дополнительной константой формулируется исчисление LD. Доказана теорема о корректности LD относительно окрестностных а-шкал.

Кроме того устанавливается связь фрагментов логики LD с известной логикой S4 [15]. В частности, модальные фрагменты с одной модальностью □< или □< совпадают с S4.

В параграфе 1.3 доказано, что топологическая модальность □ может быть выражена через временные связки. Поэтому естественно рассматривать □ как сокращение. Исчисление, полученное таким образом из LD, обозначается через La;.

Вводится еще одно исчисление L' языка временной логики с дополнительной константой {3, которое, как оказывается, является синтаксически эквивалентным исчислению La.

Для доказательства финитной аппроксимируемости L° в параграфе 1.4 введены вспомогательные Т-шкалы (с дополнительным отношением Т). Здесь следует заметить, что конечными а-шкалами эти логики нельзя аппроксимировать,так как в конечных «-пространствах, как следует из [1], отношения < и -< совпадают.

Финитная аппроксимируемость исчисления LD доказывается методом фильтраций (впервые предложенным Леммоном [20], Сегербергом [26], [27]). При этом строится фильтрация канонической модели для LD через некоторое конечное множество Ф и доказывается, что построенная фильтрация основана на Т-шкале. Следовательно, по теореме о полноте исчисления LD относительно Т-шкал (теорема 1.4.2), построенная фильтрация является моделью для LD. Разрешимость L' следует из разрешимости L°, ввиду предложений 1.3.4, 1.3.5

В главах 2 и 3 исследуются модальная и временные логики, связанные с линейно упорядоченными /-пространствами Ершова. Известна следующая теорема [2]:

Теорема Тройка (X, Хо, <} определяется /- пространством тогда и только тогда, когда выполнены условия:

1) Х0 С X;

2) отношение < является частичным порядком на X;

3) если xq,x'q £ Хо и существует х G X такой, что хо < х и х'0 < х, то в Хо имеется элемент x'q = хо U х'0;

4) для любого элемента х 6 X существует элемент хо Е Хо такой, что хо < х;

5) для любых элементов х, у G X, если х у, то существует элемент хо 6 Хо такой, что xq < х и хо ^ у.

В параграфе 2.1 вводятся понятия строго линейно упорядоченной /шкалы и строго линейно упорядоченной /о-шкалы. Тройка (X, Хо, R) называется строго линейно упорядоченной /-шкалой, если выполнены условия:

1) С X;

2) R является строгим линейным порядком;

3) xRy Зяо 6 Хо( xRxо и ( xqRy или хо = у ) );

4) для любого х € X существует хо £ Xq такой, что xqRx или = х.

Шкала (X, Хо, R) является строго линейно упорядоченной /ошкалой , если выполнены условия 1)-3) и условие

4о) существует xq € Хо такой, что для любых х G Хверно xqRx или Xq = х.

Для шкал такого вида в главе 2 рассматривается язык модальной логики с одним модальным оператором и в главе 3 — язык временной логики, с двумя модальностями Пд и Пд. Заметим, что модальности □, □< выразимы через Пд и Пд на рассматриваемых шкалах.

Подчеркнем, что в языке модальной логики с одной модальностью Пд строго линейно упорядоченные /-шкалы и строго линейно упорядоченные /о-шкалы не различаются (теорема 2.3.1). Однако в языке временной логики эти классы шкал различимы (предложение 3.1.1).

В параграфе 2.1 формулируется исчисление Lf.

Кроме того, в параграфе 2.1 вводится понятие F-шкалы. Главным результатом в главе 2 является теорема о полноте исчисления Lf относительно строго линейно упорядоченных /-шкал и строго линейно упорядоченных /о-шкал:

Теорема 2.3.1 Для любой формулы А следующие условия эквивалентны:

1) формула А выводима в исчислении Lf;

2) А истинна во всех строго линейно упорядоченных /о - моделях;

3) А истинна во всех строго линейно упорядоченных / - моделях.

Корректность исчисления Lf доказывается в параграфе 2.1. Для доказательства полноты требуются вспомогательное понятие F-шкал и дополнительное построение. Известно [10], что если формула невыводи-ма в исчислении, то она опровергается в некотором мире канонической модели этого исчисления. Следовательно она опровергается в порожденной этим миром подмодели канонической модели. Но каноническая модель для Lf не является строго линейно упорядоченной /-моделью, хотя и удовлетворяет некоторым свойствам таких моделей. Главная трудность в том, что в канонической модели отношение R, вообще говоря, не обязано быть строгим линейным порядком. Заметим, что для получения строго линейно упорядоченной /-модели в работе используется метод, аналогичный технике "раскатывания" ("bulldozing") [26]. Но задача усложняется тем, что необходимо заботиться о выполнении условий 3), 4), 40).

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

В параграфе 2.4 доказывается финитная аппроксимируемость Lf конечными F-шкалами.

В главе 3 со строго линейно упорядоченными /-шкалами мы связываем временную логику. В параграфе 3.1 вводятся исчисления L*f и L*fo, и доказывается корректность L*f относительно строго линейно упорядоченных /-шкал и корректность L*fo относительно строго линейно упорядоченных /о-шкал.

В параграфе 3.3 доказывается главный результат главы:

Теорема 3.3.1

1) Формула А выводима в исчислении L*f тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /-моделях.

2) Формула А выводима в исчислении L*fo тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /о-моделях.

Для доказательства полноты используется техника, аналогичная технике доказательства полноты Lf в главе 2. Но построения более громоздкие, так как язык содержит, кроме Пд, еще модальность прошлого п*

R'

В параграфе 3.4 методом фильтраций доказывается финитная аппроксимируемость и, следовательно, разрешимость логик L*f и L*fo. Здесь необходимо заметить, что аппроксимировать эти логики конечными строго линейно упорядоченными /-шкалами невозможно.

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

Список литературы диссертационного исследования кандидат физико-математических наук Мурзина, Вета Федоровна, 2003 год

1. Ершов Ю.Л. Теория А - пространств. Алгебра и логика, 1973, т. 12, 4, 369-418.

2. Ершов Ю.Л. Теория нумераций. Новосибирск, 1973, ч. 2, 169 с.

3. Ершов Ю.Л. Теория нумераций. М., Наука, 1977, 416 с.

4. Ершов Ю.Л. Определимость и вычислимость. Новосибирск, 1996, 300 с.

5. Куратовский К. Топология, Т.1.М., Мир, 1966

6. Расёва Е., Сикорский Р. Математика метаматематики, М.: Наука, 1972, 591 с.

7. Фейс Р. Модальная логика, М.: Наука, 1974, 520 с.

8. Шехтман В. Б.Модальные логики топологических пространств. Диссертация на соискание уч. степени доктора физ.-мат. наук, Москва, 1999

9. J. van Benthem. Temporal Logic, Handbook of Logic in Artificial Intelligence and Logic Programming, v.4, Oxford Science Publications. Oxford, Clarendon press,1995, 241-350

10. Chagrov A., Zakharyaschev M. Modal logic. Oxford University Press, 1997

11. Dummet M., Lemmon E. Modal logic between S4 and S5. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 1959, v.3, 250-264

12. Ershov Yu.L. La theorie des enumeration. Actes Congr. Intern. Math. 1 Gauthier-Villars Paris, 1971, 223-227

13. Ershov Yu.L. Theory of Domains and Nearby. Intern. Conference Formal Methods in Programming and Their Applications, Novosibirsk, Russia. Lec. Not. in Сотр. Sci. 735, Springer Verlag, 1993, 1-7.

14. Gabbay D. M. General filtration methods for modal logic. Journal of Philosophical Logic, 1972, v.l, 29-34

15. Gabbay D. Investigations in Modal and Tense Logics with Applications Problems in Philosophy and Linguistics. Cloth. Dfi., 1976, 306 p.

16. Goldblatt R. Logics of Time and Computation. CSLI Lecture Notes 7. The Chicago University Press, Chicago, 1987

17. Halpern, J., Moses, Y. Towards a theory of knowledge and ignorance. Logics and Models of Concurrent Systems,Springer, Berlin, 1985, 459476.

18. Kripke S. A completeness theorem in modal logic. Journal of Symbolic Logic, 1959, v.24, 1-14

19. Kripke S. Semantical analysis of modal logic, I. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 1963, v.9, 6796

20. Lemmon E.J. Algrbraic Semantics for Modal Logics I. The Journal of Symbolic Logic, 1966, 31:46-65

21. McKinsey J., Tarski A. The algebra of topology. Annals of Mathematics, 1944, v. 45, 141-191

22. Pratt V. Time and Information in Sequential and Concurrent Computation // Intern Workshop TPPP'94. Sendai, Japan.1.c. Not. in Сотр. Sci. 907, Springer Verlag, 1994, 1-24

23. Prior A. Past, Present and Future. Oxford University Press, 1967

24. Scott D. Advice on modal logic. In Philosophical Problems in Logic. Some Recent Development, ed. K. Lambert. Reidel, 1970, 143-172

25. Scott D. Outline of "Mathematical Theory of Computation". Fourth Annal Princeton Conf. Inform. Sci. and Systems, 1970, 97-136.

26. Segerberg K. An Essay in Classical Modal Logic, Filosofiska Studier. Uppsala Universitet,1971, v.13, 250 p.

27. Segerberg K. Decidability of S4.1. Theoria, 1968, 34:7-20

28. Shehtman V. Modal logic of domains on the real plane. Studia Logica, v. 42, 1, 63-80

29. Tarski A., Jonsson B. Boolean algebgas with operators, part 1. American Journal of Mathematics, 1951, v.73, 891-939

30. Vakarelov D. Many Dimensional Arrow Logics, J. of Applied Non -Classical Logics. - Hermes, France, 1996, v.6, 4, 303-346.

31. Vakarelov D. Modal Logics for Knowledge Representation Systems // Preprint N7. Sofia Univ., 1988, 29 p.

32. Мурзина В. Ф. Полимодальная логика на основе Л-пространств. Материалы XXXVII МНСК "Студент и научно-технический прогресс": Математика, Новосибирск, НГУ, 1999, стр. 107

33. Мурзина В. Временные логики, основанные на Л-пространствах, Логика и Приложения, Тезисы международной конференции, посвященной 60-летию академика Ю. Л.Ершова, Новосибирск, 2000, стр. 73

34. Мурзина В. Ф. Временные логики, полные относительно строго линейно упорядоченных /-моделей, Вестник НГУ, серия: Математика, механика, информатика, т.З, выпуск 1, Новосибирск, 2003, 61-82

35. Мурзина В. Ф. Модальная логика на основе линейно упорядоченных /-пространств, Алгебра и логика, т.42, 3, 2003, 320-337

36. Murzina V.F. The polymodal logic based on A spaces// Preprint 73 - 2000, IIS SB RAS, Novosibirsk, 15 p.

37. Murzina V.The completeness theorem for modal logic based on linearly ordered /о-spaces. Colleqium Logicum, Annals of Kurt-Godel-Society, Vienna, 2001, v.4, p.137; Bulettin of Simbolic Logic, v.8, 1, 2002, p. 173

38. Murzina V.The completeness theorem for temporal logic based on strictly ordered /-spaces. Logic Colloquium 2003, Helsinki, Finland, p. 126