О некоторых классах многомерных модальных логик

Первые модальные исчисления были созданы Льюисом [19], [20]. В дальнейшем теория модальностей превратилась в раздел математической логики благодаря работам Гёделя [12], Маккинси-Тарского [22], Крипке [16], [17], [18] и других. Появление многочисленных приложений модальных логик в информатике [23], теории искусственного интеллекта [5], математической лингвистике [2] и в основаниях математики [3] привело к стремительному росту этой области начиная с 1980;х годов.

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

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

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

Простейший способ комбинирования модальный логик — это их соединение, которое строится как наименьшая модальная логика в объединении языков исходных модальных логик (при этом считаем, что модальности в комбинируемых логиках обозначаются по-разному), содержащая данные исходные логики. Как показано в [6], при соединении сохраняются многие свойства исходных логик, включая полноту по Крипке, финитную аппроксимируемость и разрешимость. Однако, как показала Спаан [31], алгоритмическая сложность при соединении может вырасти.

Другой распространённый вид комбинирования — это произведения, которые могут использоваться для описания «прямых произведений» различных модальных структур, например, пространства и времени, действий и времени, действий и необходимости и т. д. Произведение модальных логик определяется как логика класса всевозможных прямых произведений шкал Крипке перемножаемых логик (под прямым произведением шкал понимается шкала, носителем которой является прямое произведение носителей перемножаемых шкал, а в качестве отношений берутся отношения исходных шкал, продолженные на новые измерения как отношения равенства). Данный метод построения модальных логик был впервые рассмотрен Шехтманом [40] и в дальнейшем подробно изучен в ряде работ [7], [8], [9], [10], [30]. Произведения модальных логик применяются в информатике и в теории искусственного интеллекта ([25], [26], [27], [7], также с произведениями тесно связаны результаты о многомерных дескриптивных модальных логиках [32]).

В дополнение к обычному произведению модальных логик (называемому также семантическим) определяется синтаксическое произведение, строящееся при помощи добавления к соединению перемножаемых логик аксиом специального вида. Как показано в [8], синтаксическое и семантическое произведения двух «хорновских» модальных логик совпадают, откуда следует, что для достаточно широкого класса модальных логик их произведение можно задать аксиоматически добавлением к исходным логикам дополнительных аксиом (модальные логики, семантическое и синтаксическое произведения которых совпадают, называются «просто перемножаемыми»).

Однако, эти произведения совпадают не всегда, например, как показано в [8], семантическое и синтаксическое произведения логик Grz С L С Triv и S4 С L2 С Triv не совпадают. В связи с этим для модальных логик актуален вопрос — совпадают ли их синтаксическое и семантическое произведения, т. е., можно ли аксиоматизировать их семантическое произведение с помощью аксиом их синтаксического произведения.

Перенос различных свойств модальных логик (табличности, финитной аппроксимируемости, конечной аксиоматизируемости, разрешимости и некоторых других) от сомножителей к произведениям исследовался в ряде работ (см. [7]), например, в [8]. В частности, было показано, что конечная аксиоматизируемость, финитная аппроксимируемость и разрешимость в общем случае не переносятся, табличность переносится, для рекурсивной аксиоматизируемости показано, что она переносится для некоторых классов перемножаемых логик.

В [11] показано, что произведение двух логик из достаточно широкого класса, включающего, в частности, К4, S4, Grz, GL, неразрешимо и не является финитно аппроксимируемым. Как следует из [13], при п ^ 3 все модальные логики, находящиеся между Kx. xKhS5x.x S5, являются v v / s V ^ п п неразрешимыми и не могут быть конечно аксиоматизированы. Эти результаты показывают, что произведение даже простых логик может иметь очень сложную структуру, причём для высоких размерностей ситуация ухудшается.

Для разрешимых произведений модальных логик возникает вопрос об их сложности. Во многих случаях сложность при умножении логик возрастает [7], например, произведения К4 х К и К4 х S5 coNEXPTIME-трудны, S5 х S5 и S5 х К — coNEXPTIME-полны, К4.3 х S5 — EXPSPACE-трудно. Однако в работе Маркса [21] показано, что сложность произведения логики класса одномодальных шкал Крипке F с функциональной модальностью (в действительности, такими логиками являются в точности непротиворечивые расширения логики SL, речь о которой пойдёт ниже) на логику класса одно-модальных шкал Крипке /С совпадает со сложностью логики данного класса.

С.

Модальные логики «завтра» (SL) и «вчера-завтра» (SL.t) (называемые также логиками с функциональными модальностями благодаря специфической структуре их шкал Крипке) были введены в 1965 году Леммоном и Скоттом (также см. [24]). Доказательства же первых результатов об этих логиках были опубликованы Сегербергом [29], а Мучник [34], [35] доказал предтабличность логик SL и SL. t (т.е., что все непротиворечивые собственные расширения этих логик есть логики конечных шкал Крипке) и получил полное описание их расширений. Но систематическое исследование логик с функциональными модальностями было начато только в работе Сегербер-га [28] и продолжено Белиссимой [1] и Крахтом [15].

Многомодальные логики с функциональными модальностями являются естественным обобщением логики «завтра» (а логика «вчеразавтра» является их частным случаем). Семейство этих логик очень велико — можно легко построить неразрешимые модальные логики такого вида и, более того, нет возможности построить их разумную классификацию [15, параграф 9.4]. Некоторые логики из этого семейства — многомерные варианты SLn логики SL — были рассмотрены Габбаем и Шехтманом [8]. В частности, в этой работе было показано, что любые семейства соединений произвольного количества логик SL финитно аппроксимируемы (и, как следствие, разрешимы) и являются просто перемножаемыми, откуда следут, что логики SLn есть логики семейства всех шкал с п коммутирующими функциональными модальностями.

Многомодальный вариант логики SL представляет интерес как фрагмент пропозициональной динамической логики детерминированных вычислений DPDL [15]. Также многомодальные логики с функциональными модальностями применяются в математической лингвистике [2], [14].

При рассмотрении многомерного варианта SLn логики SL возникли естественные вопросы:

1) Как для случая логики SL" выглядят аналоги результатов, полученных Мучником [34], [35] для SL ?

2) Обобщаются ли результаты Маркса [21] о сложности проблемы выполнимости для произведения класса одномодальных функциональных шкал Крипке Т на класс одномодальных шкал Крипке К на классы Т многомодальных функциональных шкал Крипке и многомодальные классы /С ?

3) Что можно сказать о переносе свойств для произведений модальных логик на логики с коммутирующими функциональными модальностями ?

4) Переносится ли результат Габбая и Шехтмана [8] о простой перемно-жаемости семейств соединений произвольного количества логик SL на произведения многомерных логик с функциональными модальностями на произвольные многомодальные логики ?

5) Насколько сходны между собой многомерные варианты SLn и SL. t" логик «завтра» SL и «вчера-завтра» SL. t ?

Цель работы.

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

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

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

1) Доказана конечная аксиоматизируемость всех расширений SLn и предложена их стандартная аксиоматизация.

2) Доказана разрешимость всех расширений SL", приведён алгоритм решения проблемы выводимости для SLn и доказана разрешимость таб-личности расширений SLn.

3) Установлено, что все расширения SL™ являются финитно аппроксимируемыми.

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

5) Найдено достаточное условие простой перемножаемости полных модальных логик и расширений SLn и критерий простой перемножаемости логик Кот и расширений SLn.

6) Для расширений SL. t™ дано более простое (по сравнению со случаем расширений SL") доказательство их финитной аппроксимируемости и предложена их стандартная аксиоматизация.

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

Результаты диссертации докладывались и обсуждались в 2000;2005 г. на научно-исследовательском семинаре по математической логике под руководством академика РАН С. И. Адяна и профессора В. А. Успенского и других спецсеминарах кафедры математической логики и теории алгоритмов механико-математического факультета МГУ, на международной конференции «Computer science applications of modal logic» (Москва, 2005), на XXIV.

Конференции молодых учёных (Москва, 2002), на международном семинаре «2nd Moscow-Vienna Workshop on Logic and Computation» (Москва, 2002) и были представлены на международной конференции «ASL Logic Colloquium» (Вена, 2001). По теме диссертации автором опубликованы работы [41]-[47].

Содержание работы.

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

Первая глава содержит вспомогательный материал. Здесь даются необходимые определения, связанные с модальными логиками, и формулируются некоторые известные результаты. Параграф 1.7 посвящён теории базисов Грёбнера для полиномиальных колец над Q.

Во второй главе исследуются свойства расширений SLn. В параграфах 2.1 и 2.2 устанавливается каноническое соответствие между 8Ьп-конусами и конгруэнциями на Мп и доказываются его свойства.

В параграфе 2.3 каждой конгруэции на Nn сопоставляется идеал кольца полиномов от п переменных с рациональными коэффициентами:

Определение (2.11). Пусть ~ - конгруэнция на Jfn. Положим и доказывается его свойство Лемма (2.15). Если ~ - конгруэнция uaNn, то ха — хъ е V Н, а ~ Ь.

В параграфе 2.4 установлена взаимосвязь между аксиомами логик SLn-конусов, порождающими разностями мономов идеалов вида V (~) и порождающими элементами конгруэнций на Jfn.

Отсюда получается способ построения аксиом логик конусов SLn:

Лемма (2.24). Пусть С — SLп-конус. Тогда найдутся векторы aj, bj € Nn, 1 ^ г ^ к, к ^ 0, такие что к.

С© = SLn + Д (Da.

В параграфе 2.5 доказывается теорема о нормальной форме в логике SL". В параграфе 2.6 доказано, что конечно аксиоматизируемые расширения SLn являются логиками конечного числа SLn-K0iiyc0B.

В параграфе 2.7 определяется приведённый вид формул SLn:

Определение (2.34). Будем говорить, что п-модальная формула, А находится в приведённом виде, если к TTT-i.

А = V Д = i=l 3=1 для некоторых k ^ 0, а^, b^ € Nn, где l^i^k, rrii, mi ^ 0. и доказывается, что.

Теорема (2.35). Kaotcdoe конечно аксиоматизируемое расширение SLn аксиоматизируется формулой в приведённом виде.

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

Теорема (2.39). Kaotcdoe конечно аксиоматизируемое расширение SLn аксиоматизируется формулой во вполне приведённом виде. При фиксированном порядке па мономах эта формула единственна с точностью до перестановок дизъюнктивных и конъюнктивных членов.

В параграфе 2.8 с помощью леммы Кёнига доказывается конечная аксиоматизируемость всех расширений SLn.

В параграфе 2.9 доказан алгоритмический вариант теоремы 2.39:

Теорема (2.48). Для п-модальной формулы A mooicho алгоритмически построить п-модальную формулу В во вполне приведённом виде, такую что.

SLn + А = SLn + В. Отсюда получаются следствия: Теорема (2.50). Проблема выводимости для логики SLn разрешима. Теорема (2.51). Каждое расширение SLn разрешимо.

В параграфе 2.10 доказано (теорема 2.57), что по аксиоме расширения логики SLn можно алгоритмически распознать, является ли оно табличным. Дальнейшая часть второй главы посвящена доказательству теоремы 2.82:

Теорема (2.82). Все расширения логики SLn финитно аппроксимируемы.

В третьей главе рассматриваются свойства произведений расширений SLn и полных по Крипке многомодальных логик. В этой главе L — это непротиворечивое расширение логики SLn, Л — непротиворечивая полная по Крипке ш-модальная логика. Модальности в, А обозначаются как.

В параграфе 3.1 мы вводим определение перевода (п+т)-модальной формулы в т-модальную:

Определение (3.1). Распространим определения ф{А) и (Г {А), 1 < i ^ п, (а, значит, и определения d (А) и D (А)) на формулы в языке L х, А добавлением следующих правил: ф {ЩА) Щф (A), dl {ЩА) ±=- dl (А).

Пусть А{р,., pk) — формула в языке L х А, ~ - конгруэнция на Afn. Полооюим.

А~^ф (А) (?]*%).а. и доказываем основное свойство этого перевода.

Лемма (3.2). Пусть С — SLп-конус, F — т-модальная шкала Крипке, Аформула в языке L х А. Тогда.

С х F= А&-F=.

Используя это свойство, мы показываем, что для семантического произведения рассматриваемых логик финитная аппроксимируемость сохраняется:

Теорема (3.3). Логика, А финитно аппроксимируема тогда и только тогда, когда логика L х, А финитно аппроксимируема.

В параграфе 3.2 мы изучаем разрешимость семантического произведения данных логик. Для этого мы показываем, что произведение L х, А т-сводится (как множество формул) к А:

Лемма (3.4). Пусть L = С{С,., Сгде С, ., С^ - SLп-конусы. Пусть, А — формула в языке L х А. Тогда.

ЬхАНЛ<^А1-Д .

При помощи этой леммы мы показываем, что.

Теорема (3.5). Логика Л разрешима тогда и только тогда, когда логика L х Л разрешима.

Также мы может оценить сложность разрешающего алгоритма для произведения:

Теорема (3.7).

1) По аксиоме логики L и разрешающему алгоритму для логики, А можно построить разрешающий алгоритм для логики L х Л.

2) Если для логики Л существует разрешающий алгоритм, время работы которого на формулах длины не более I не превосходит fi (l), а используемая память не превосходит то для логики L х Л можно построить разрешающий алгоритм с соответствующими верхними оценками k{fi (l) + gi (l), где ki — константы, a gi — полиномы.

В параграфе 3.3 сравниваются различные произведения указанных логик. Мы получаем достаточное условие простой перемножаемости:

Теорема (3.8). Если L — логика конуса, то.

L, Л] = L х Л. и критерий простой перемножаемости для Л = Кт:

Теорема (3.10). При т ^ 1 условие.

L, Кт] = L х Кт равносильно тому, что L является логикой единственного конуса.

В четвёртой главе мы рассматриваем расширения логики SL.tn. Мы показываем, что решётка расширений логики SL. tn связана с подгруппами Zn подобно тому, как решётка расширений логики SLn связана с конгруэнци-ями на ЛЛ Используя эту связь, мы приводим более простое, чем для общего случая расширений SLn, доказательство финитной аппроксимируемости расширений логики SL. t" .

В параграфе 4.3 доказан следующий результат:

Лемма (4.14). Пусть М — подгруппа Zn, а- 6 Z", U г О, — векторы. Тогда условие к.

C (Ct (M)) = SL. tn + /(p = D? p) i=1 эквивалентно тому, что М порождена всеми векторами aj.

Здесь Ct (М) — SL. tn-Konyc, соответствующий подгруппе М.

Отсюда получается способ аксиоматизации логик конусов SLn:

Лемма (4.15). Пусть С — SL. tп-конус. Тогда найдутся векторы гц е Zn- 1 < % ^ к, к ^ 0, такие что к.

С© = SL. t" + Д (р = од. г=1.

Дальнейшие результаты четвёртой главы аналогичны соответствующим результатам второй главы.

В приложении, А из полученных ранее результатов выводятся теоремы Мучника [35]:

Теорема (А.7). Собственные расширения логик SL и SL. t табличны. Теорема (А.8).

1) Пусть L — собственное расширение SL, тогда.

L — SL + A (mi, ?ii) U. U, А щ), где k ^ 0. Если при этом логика L аксиоматизируется формулой А, то для каждого г rrii + rii < d1 (А).

2) Пусть L — собственное расширение SL. t, тогда.

L = SL. t + At (ni) U. U At {nk), где k ^ 0. Если при этом логика L аксиоматизируется формулой А, то для каэ/сдого г.

Здесь, А (га, п) и А* (п) — формулы следующего вида:

Определение (А.2). Для т, п (Е N, п > 0, определим одномодалъную формулу, А (га, п) как.

А (га, п) ±-=г? тр =? т+пр. Для п? Nп > 0- определим бимодальную формулу At (п) как.

At {п)^р = UnlP.

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

1. Bellissima F. On the lattice of extensions of the modal logics K. Altn. Arch. Math. Logic, 1988, Vol. 27, No. 2, P. 107−114.

2. Blackburn P., Bos J. Representation and Inference for Natural Language: A First Course in Computational Semantics. CSLI Press, Stanford, 2005.

3. Boolos G. The Logic of Provability. Cambridge University Press, 1993.

4. Chagrov A. V., Zakharyaschev M. V. Modal Logic. In: Oxford Logic Guides, Oxford University Press, 1997, Vol. 35.

5. Fagin R., Halpern J., Moses Y., Vardi M. Reasoning about Knowledge. MIT Press, 1995.

6. Fine K., Schurz G. Transfer theorems for stratied modal logics. J. Copeland, editor, Logic and Reality, Essays in Pure and Applied Logic. In memory of Arthur Prior, Oxford University Press, 1996, P. 169−213.

7. Gabbay D., Kurucz A., Wolter F., Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications. In: Studies in Logic and the Foundations of Mathematics, Elsevier, North-Holland, 2003, Vol. 148.

8. Gabbay D., Shehtman V. Products of modal logics, part 1. Logic Journal of the IGPL, 1998, Vol. 6, No. 1, P. 73−146.

9. Gabbay D., Shehtman V. Products of modal logics. Part 2: Relativised quantifiers in classical logic. Logic Journal of the IGPL, 2000, Vol. 8, No. 2, P. 165−210.

10. Gabbay D., Shehtman V. Products of modal logics. Part 3: Products of modal and temporal logics. Studia Logica, 2002, Vol. 72, No. 2, P. 157−183.

11. Gabelaia D., Kurucz A., Wolter F., Zakharyaschev M. Products of 'transitive' modal logics. Journal of Symbolic Logic, 2005, Vol. 70, No. 3, P. 9 931 021.

12. Godel K. Eine Interpretation des intuitionistischen Aussagenkalkiils. Ergebnisse eines mathematischen Kolloquiums, 1933, Vol. 4, P. 39−40.

13. Hirsch R., Hodkinson I., Kurucz A. On modal logics between К x К x К and S5 x S5 x S5. Journal of Symbolic Logic, 2002, Vol. 67, P. 221−234.

14. Kracht M. Highway to the danger zone. Journal of Logic and Computation, 1995, Vol. 5, P. 93−109.

15. Kracht M. Tools and techniques in modal logic. In: Studies in Logic and Foundations of Mathematics, Elsevier, North-Holland, 1999, Vol. 142.

16. Kripke S. A. A completeness theorem in modal logic. Journal of Symbolic Logic, 1959, Vol. 24, P. 1−14.

17. Kripke S.A. Semantical analysis of modal logic, Part I. Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 1963, Vol. 9, P. 6796.

18. Kripke S. A. Semantical considerations on modal logic. Acta Philosophica Fennica, 1963, Vol. 16, P. 83−94.

19. Lewis C. A Survey of Symbolic Logic. University of California Press, Berkeley, 1918.

20. Lewis C., Langford C. Symbolic Logic. Appleton-Century-Crofts, New York, 1932.

21. Marx M. Complexity of products of modal logics. Journal of Logic and Computation, 1999, Vol. 9, P. 197−214.

22. McKinsey J. С. C., Tarski A. The algebra of topology. Annals of Mathematics, 1944, Vol. 45, P. 141−191.

23. Прасолов В. В. Многочлены. Москва: Издательство МЦНМО, 2001.

24. Скорняков JI. А. Элементы общей алгебры. Москва: Наука, 1983.

25. Шехтман В. Б. Двумерные модальные логики. Mam. заметки Академии паук СССР, 1978, т. 5, с. 759−772.

26. Кравцов А. Г. Наследственная конечная аксиоматизируемость логики SLn. Доклады Академии наук РФ, 2003, т. 391, вып. 1, с. 14−16.

27. Кравцов А. Г. О некоторых свойствах произведений модальных логик. Москва: МГУ, 2005. 46 с. Рукопись депонирована в ВИНИТИ 03/03/2005, К0- 303-В2005.

28. Кравцов А. Г. Об одном семействе разрешимых модальных логик. Успехи математических наук, 2002, т. 57, вып. 4, с. 179−180.

29. Кравцов А. Г. Разрешимость табличности для расширений SLn. Труды XXIV Конференции молодых учёных механико-математического факультета МГУ им. М. В. Ломоносова, 2002, с. 93−95.

30. Kravtsov A. G. Extensions of multidimensional successor logics. Computer science applications of modal logic, 2005, P. 22−23.

31. Kravtsov A. G. Extensions of multidimensional temporal logics. Bulletin of Symbolic Logic, 2002, Vol. 8, No. 1, P. 124.

32. Kravtsov A. G. Polymodal logics of commuting functions. Logic Journal of the IGPL, 2002, Vol. 10, No. 5, P. 517−533.