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

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

КРАВЦОВ АЛЕКСЕЙ ГЕННАДИЕВИЧ

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

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

Автореферат

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

Москва - 2006

/

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

Научный руководитель: доктор физико-математических

наук, профессор В. Б. Шехтман

Официальные оппоненты: доктор физико-математических

наук, профессор А. В. Чагров кандидат физико-математических наук, доцент А. А. Мучник

Ведущая организация: Математический Институт

имени В. А. Стеклова Российской Академии Наук

Защита диссертации состоится 12 мая 2006 г. в 16 ч. 15 мин. на заседании диссертационного совета Д.501.001.84 в Московском государственном университете имени М.В. Ломоносова по адресу 119992, ГСП-2, Москва, Ленинские горы, МГУ, механико-математический факультет, аудитория 14-08.

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

Автореферат разослан 12 апреля 2006 г.

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

Н. Чубариков

"7570

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

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

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

Логика модальностей была известна ещё в античные времена, и на протяжении долгого времени её изучение велось в рамках гуманитарных дисциплин. Формальные модально-логические исчисления появились лишь в начале 20-го века в работах К. Льюиса, а с математической точки зрения модальности начали исследоваться в 1940-1950 гг. К. Геделем, А. Тарским, Дж. Маккянси, С. Крипке и др. Многочисленные приложения модальных логик в теории искусственного интеллекта, информатике, математической лингвистике н основаниях математики вызвали стремительный рост исследований в данной области. Модальная логика в её современном виде представляет собой сложившуюся математическую дисциплину, имеющую собственные задачи и методы и связанную с другими областями математики, в том числе с универсальной алгеброй, теорией категорий и общей топологией.

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

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

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

Простейший способ комбинирования модальных логик - это их соединение. Оно строится как наименьшая модальная логика в объединении языков исходных логик, содержащая данные логики (при этом считаем, что модальности в комбинируемых логиках обозначаются по-разному). Как доказано в работах Файна-Шурца1 и Крахта-Волтера2, при соединении сохраняются многие свойства исходных логик, включая полноту по Крипке, финитную аппроксимируемость и разрешимость. С другой стороны, как показала Э. Спаан3, алгоритмическая сложность при соединении может вырасти.

Другой распространённый вид комбинирования - это произведения модальных логик. Они используются для описания «прямых произведений» различных модальных структур, например, при формализации пространства и времени, действий и времени, действий и знания и т. д. Произведение модальных логик определяется как логика класса всевозможных произведений вида F х G, где F и G - шкалы Крипке исходных логик (произведение шкал определяется естественным образом). Данный метод построения модальных логик был впервые предложен В. Б. Шехт-маном4 и в дальнейшем подробно исследован8'8,т. Произведения модальных логик тесно связаны с другими типами логик, применяемых в современной информатике и теории искусственного интеллекта, в частности, в теории представления знаний6.

Кроме «семантического» произведения модальных логик L\ XL2, описанного выше, используют также синтаксическое произведение [L\,Li\. Оно получается из соединения данных логик с помощью добавления аксиом специального вида. Как известно6,6, синтаксическое и семантическое произведения двух «хорновских» модальных логик совпадают; таким образом, для достаточно широкого класса модальных логик аксиоматика их произведения эффективно строится по аксиоматикам этих логик (во-

1Fine К., 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.

2Kracht M., Wolter P. Properties of independently axiomatizabie bimodal logics. Journal of Symbolic Logic, 1991, v. 56, p. 1469-1485.

3Spaan E. Complexity of modal logics. PhD thesis. Department of Mathematics and Computer Science, University of Amsterdam, 1993.

*Шехтман В. Б. Двумерные модальные логики. Математические заметки, 1978, т. 5, с. 759-772.

'Gabbay D., Kurucz A., Wolter F., Zakharyaschev M. Many-dimensional modal logics: Theory and applications. Elsevier, 2003.

eGabbay D., Shehtman V. Products of modal logics, part 1. Logic Journal of the IGPL, 1998, v. 6, no. 1, p. 73-146.

7Shehtman V. Filtration via bisimulation. Advances in Modal Logic, ed. R. Shmidt et

aL, King's College Publications, London, 2005, v. 5, p. 289-308.

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

Следует отметить, что вопрос о совпадении двух типов произведений модальных логик оказывается нетривиальным - так, например*, Li х L12 Ф [Li , Li] для любых пар модальных логик Grz С L\ С Triv и S4 С £2 С Triv.

Также нетривиальной оказывается проблема переноса свойств (таких, как табличность, финитная аппроксимируемость, разрешимость и др.) от модальных логик к их произведениям. Эта проблема изучалась целым рядом авторов8,®'7; так, было установлено, что в общем случае табличность переносится, а многие другие свойства, включая конечную аксиоматизи-, руемость, рекурсивную аксиоматизируемость, финитную аппроксимиру-

емость и разрешимость, не переносятся.

Из негативных результатов отметим, что при п > 3 все «многомерные» модальные логики в интервале между Kx..,xKhS5x...xS5

I > V * 4 V ^

п п

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

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

гик сложность возрастает5; например, произведение coNP-полных логик К4.3 и S5 оказывается EXPSPACE-трудным. Однако в работе М. Маркса® показано, что произведение непротиворечивой логики с одной функ-' циональной модальностью (т. е. расширения логики SL, см. ниже) на про-

извольную полную одномодальную логику L полиномиально эквивалентно L.

Модальные логики «завтра» (SL) и «вчера-завтра» (SL.t) были введены в 1965 году Э. Леммоном и Д. Скоттом10 (модальности в этих логиках называются функциональными). Свойства этих логик были исследованы К. Сегербергом11 и А. А. Мучником12'13, который доказал их

aHirsch R., Hodkinson I., Kurucz A. On modal logice between К X К X К and SB x SS x SB. Journal of Symbolic Logic, 2002, v. 67, p. 221-234. ,

9 Marx M. Complexity of products of modal logics. Journal of Logic and Computation, 1999, v. 9, p. 197-214.

10Prior A. Past, present, and future. Oxford University Press, 1967.

11Segerberg K. On the logic of tomorrow. Theoria, 1967, v. 33, p. 45-52.

12 Ермолаева H.M., Мучник А. А. Модальные логики, определяемые эндоморфизмами дистрибутивных решёток. В кн.: Исследования по неклассическим логикам, Москва: Наука, 1976, с. 229-246.

13Ермолаева Н. М., Мучник А. А. Предтаб личная временная логика. В кн.: Исследования по неклассическим логикам, Москва: Наука, 1979, с. 288-297.

предтабличность (т.е., что все непротиворечивые собственные расширения этих логик есть логики конечных шкал Крипке) и получил полное описание их расширений. Но систематическое исследование логик с функциональными модальностями (в том числе, и их многомодальных вариантов) было начато в работе К. Сегерберга14 и продолжено Ф. Белиссимой15 и М. Крахтом10.

Семейство многомодальных логик с функциональными модальностями очень велико - известны неразрешимые модальные исчисления такого вида и, более того, нет возможности построить их классификацию16. Некоторые логики из этого семейства - многомерные варианты ЭЬ" логики 8Ь - были изучены Д. Габбаем и В. Б. Шехтманом®. В частности, было показано, что эти логики финитно аппроксимируемы, разрешимы и просто перемножаемы. Отсюда следует, что ЭЪ" есть логика класса всех шкал с п коммутирующими функциональными отношениями.

Многомодальные логики с функциональными модальностями также активно используются в математической лингвистике17 и возникают как фрагменты пропозициональной динамической логики детерминированных вычислений БРБЬ18.

Цель работы

Целью данной работы является исследование расширений логики вЬ", доказательство разрешимости ряда свойств этих расширений, изучение свойств произведений расширений 8ЬП и произвольных многомодальных логик.

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

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

14Segerberg K. Modal logics with functional alternative relations. Notre Dame Journal of Formal Logic, 1986, v. 27, p. 504-522.

l8Bellissima F. On the lattice of extensions of the modal logics K.Altn. Arch. Math, logic, 1988, v. 27, no. 2, p. 107-114.

16Kracht M. Tools and techniques in modal logic. Elsevier, 1999.

17Blackburn P., Bos J. Representation and inference for natural language: A first course

in computational semantics. CSLI Press, Stanford, 2005.

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

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

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

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

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

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

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

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

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

Апробация результатов

Результаты диссертации докладывались и обсуждались в 2000-2005 гг. на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов механико-математического факультета МГУ, на Международной конференции «Приложения модальной логики в информатике» (Москва, 2005), на XXIV конференции молодых учёных мехаг нико-математического факультета МГУ (Москва, 2002), на 2-м международном семинаре «Москва-Вена» по логике и вычислимости (Москва, 2002) и были представлены на международной конференции «ASL Logic Colloquium» (Вена, 2001).

Публикации

Основные результаты диссертации опубликованы в семи работах автора (1-7], список которых приведён в конце автореферата. Работ, написанных в соавторстве, нет.

Структура диссертации

Диссертация состоит го введения, четырех глав, приложения, предметного указателя и списка литературы. Текст диссертации изложен на 115 страницах. Список литературы содержит 47 наименований.

Содержание диссертации

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

Первая глава содержит вспомогательный материал. Здесь даются необходимые определения, связанные с модальными логиками, и формулируются некоторые известные результаты. Параграф 1.7 посвящён теории базисов Грёбнера для полиномиальных колец над Q. Во второй главе исследуются свойства расширений SLn. В параграфах 2.1 и 2.2 устанавливается каноническое соответствие между 8Ьп-конусами и конгруэнциями на М" и доказываются его свойства.

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

Определение (2.11). Пусть ~ - конгруэнция на Мп. Положим

V (~) {{х* - хь | а ~ Ъ}).

и доказывается его свойство

Лемма (2.15). Если ~ - конгруэнция на Nn, то

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

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

Лемма (2.24). Пусть С - ЯЬп-конус. Тогда найдутся векторы а<,Ъ* е 1 < г ^ к, к > 0, такие что

к

С(С) = + Д =пЬ4р).

г=1

В параграфе 2.5 доказывается теорема о нормальной форме в логике 81Л

В параграфе 2.6 доказано, что конечно аксиоматизируемые расширения ЭЬ" являются логиками конечного числа вГЛ-конусов. В параграфе 2.7 определяется приведённый вид формул ЭЬ":

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

к m^

А= V Д (□■«Й = ПЬ«Л) ¿=11=1

для некоторых к^О, а^, Ь^ 6 14", где 1 < г < к, 1 < ] < тг, тг > 0. и доказывается

Теорема (2.35). Каждое конечно аксиоматизируемое расширение 8ЬП аксиоматизируется формулой в приведённом виде.

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

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

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

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

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

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

Э1,п + А = ЯЬ" + в.

Отсюда получаются следствия:

Теорема (2.50). Проблема выводимости для логики вЬ" разрешима.

Теорема (2.51). Каждое расширение ЭЬ" разрешимо.

В параграфе 2.10 доказано (теорема 2.57), что по аксиоме расширения логики ЭЬП можно алгоритмически распознать, является ли оно табличным.

Дальнейшая часть второй главы посвящена доказательству теоремы 2.82:

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

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

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

Определение (3.1). Распространим определения ф(А) и <1* (А), 1 ^ г < п, (а, значит, и определения с! (Л) и О (А)) на формулы в языке Ь х Л добавлением следующих правил: ф(№.,А) ^ Щф{А), сГ (В^А) ^ 6* (А).

Пусть А(р1, ...,рк) - формула в языке Ь х Л, ~ - конгруэнция на Мп. Положим

и доказываем основное свойство этого перевода

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

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

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

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

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

LxA\-A*>Ah 1\А~С<.

i

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

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

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

Теорема (3.7).

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

S) Если для логики А существует разрешающий алгоритм, время работы которого на формулах длины не более I не превосходит fi{l), а используемая память не превосходит /г (0, 1710 для логики L х А можно построить разрешающий алгоритм с соответствующими верхними оценками kifi(l) +ffi(l), где fc, - константы, agi - полиномы.

В параграфе 3.3 мы получаем достаточное условие простой перемно-жаемосги:

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

[L,A] = IxA.

и критерий простой перемножаемости для А = Кт:

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

[Li Km] = L х Km

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

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

Лемма (4.14). Пусть М - подгруппа 2п, а, € Ъп, 1 < г < к, - векторы. Тогда условие

к

ЦСг (М)) = ЗЬЛЯ + /\(р= ПГр) »=1

эквивалентно тому, что М порождена всеми векторами а1.

Здесь Се (М) - ЭЬ.^-конус, соответствующий подгруппе М.

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

Лемма (4.15). Пусть С - 8Ъ±п-конус. Тогда найдутся векторы а, е 2П, 1 < г < к, к ^ 0, такие что

к 1=1

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

В приложении А из результатов предыдущих глав получаются новые доказательства теорем Мучника13:

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

1) Пусть Ь - собственное расширение вЬ, тогда

Ь = + А (тх, п\) и... и А (т/ь, Пк),

где к>0. Если при этом логика Ь аксиоматизируется формулой А, то для каждого г

тг + гц < ¿I1 (Л).

2) Пусть Ь - собственное расширение тогда

Ь = + А* (щ) и...иА, (п*),

где к > 0. Если при этом логика Ь аксиоматизируется формулой А, то для каждого г

щ

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

Определение (А.2). Для т,п € 14, п > 0, определим одномодальную формулу А (т, п) как

А (т, п) Отр = От+пр. Для п € 14, п > 0, определим бимодальную формулу А( (п) кок

Ае(п) =

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

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

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

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

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

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

[5] Kravtsov A. G. Extensions of multidimensional successor logics. International conference "Computer science applications of modal logic", Moscow, September 5-9, 2005, Abstracts, Москва: МЦНМО, 2005, p. 22-23.

[6] Kravtsov A. G. Extensions of multidimensional temporal logics. Bulletin of Symbolic Logic, 2002, v. 8, no. 1, p. 124.

[7] Kravtsov A. G. Polymodal logics of commuting functions. Logic Journal of the IGPL, 2002, v. 10, no. 5, p. 517-533.

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

Формат 60x90 1/16. Усл. печ. л. QJÇ

Тираж //Û3K3. Заказ

¿OCXoft 7 BIO

-7 5 70

Введение

1. Обзор используемых определений и результатов

1.1. Общие определения

1.2. Операции над отношениями.

1.3. Модальные логики.

1.4. Шкалы Крипке.

1.5. Произведения модальных логик

1.6. Временные логики.

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

2. Свойства расширений логики SLn

2.1. Действия моноидов и левые конгруэнции.

2.2. Связь 8Ьп-конусов и конгруэнций на Ып.

2.3. Конгруэнции на Мп и идеалы кольца полиномов над Q.

2.4. Конгруэнтные замыкания множеств пар векторов.

2.5. Нормальные формы в SLn

2.6. Описание конечно аксиоматизируемых расширений SLn.

2.7. Приведённый вид аксиом расширений SLn.

2.8. Конечная аксиоматизируемость расширений SLn.

2.9. Разрешимость расширений SLn.

2.10. Разрешимость табличности конечно аксиоматизируемых расширений SL".

2.11. Операции над конгруэнциями.

2.12. Структура классов сглаживания.

2.13. Поведение конгруэнций при склейке.

2.14. Финитная аппроксимируемость расширений SLn.

3. Свойства произведений модальных логик

3.1. О сохранении финитной аппроксимируемости для произведений

3.2. О сохранении разрешимости для произведений.

3.3. О простой перемножаемости

4. Свойства расширений логики SL.tn

4.1. Связь SL.tn-K0Hyc0B и конгруэнций на Zn

4.2. Связь SL.t"-KonycoB и подгрупп Zn.

4.3. Порождающие множества подгрупп Zn.

4.4. Нормальные формы в SL.t™

4.5. Финитная аппроксимируемость расширений SL.tn.

4.6. Приведённый вид аксиом расширений SL.t™.

А. Свойства логик SL и SL.t

А.1. Свойства конусов логик SL и SL.t.

А.2. Описание расширений логик SL и SL.t.10б

Предметный указатель

Первые модальные исчисления были созданы Льюисом [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). Пусть ~ - конгруэнция на J\fn. Положим и доказывается его свойство Лемма (2.15). Если ~ - конгруэнция uaNn, то ха - хъ е V Н а ~ Ь.

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

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

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

С(С) = SLn + Д (Da<p = □ hip). i=1

В параграфе 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. 9931021.

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.