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

«о

РОССИЙСКАЯ АКАДЕМИЯ НАУК СИБИРСКОЕ ОТДЕЛЕНИЕ > Со ИНСТИТУТ МАТЕМАТИКИ

' Специализированный совет Д 002.23.01

на правах рукописи УДК 517.11

ЗАХАРЬЯЩЕВ Михаил Викторович

МЕТОД КАНОНИЧЕСКИХ < 1РМУЛ И ЕГО ПРИМЕНЕНА В МОДАЛЬНОЙ ЛОГИх

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

АВТОРЕФЕРАТ диссертации на соискание учёной степени доктора физико-математических наук

Новосибирск — 1998

Работа выполнена в Институте прикладной математики им. М.В. Келдыша РАН

Официальные оппоненты:

доктор физико-математических наук, профессор Н.К. Косовский

доктор физико-математических наук, профессор Л.Л. Максимова

доктор физико-математических наук, профессор В.Л. Селиванов

Ведущая организация: Вычислительный Центр РАН

Защита состоится " 1998 г. в " ^ ^ " часов на засе-

дании Специализированного совета Д 002.23.01 при Институте математики Сибирского отделения РАН по адресу: 630090, г. Новосибирск-90, Университетский проспект, 4.

С диссертацией можно ознакомиться в библиотеке Института математики СО РАН.

/?

Автореферат разослан " ' " ^ 1998 г.

Учёный секретарь

Специализированного совета Д.002.23.01 кандидат физико-математических наук

А.Н.Ряскин

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Модальная логика — одна из наиболее динамично развивающихся ветвей математической логики, нашедшая многочисленные приложения в основаниях математики, философии, информатике, лингвистике, искусственном интеллекте и других областях. Начавшись, казалось бы, с не очень-то обоснованных систем Льюиса (1918, 1932), которые вряд ли бы заметили в серьезных математических кругах, своим нынешним положением она обязана, прежде всего, двум открытиям.

Во-первых, прочитав льюисовский оператор □ (некой абстрактной) необходимости как "доказуемо", Орлов [6] и Гёдель [28] дали классическую интерпретацию интуиционистской пропозициональной логики Int посредством погружения ее в модальную систему "доказуемости", которая к тому же оказалась эквивалентной льюисовской S4. Это открытие, с одной стороны, стимулировало установление связи модальной и интуиционистской логик с топологией и алгеброй в виде построения Стоуном [40], а также Маккинси и Тарским [35] топологической и алгебраической семантик для S4 и Int. А с другой стороны, оно продемонстрировало возможность использования модальной логики в основаниях математики для анализа феномена доказуемости в формальных системах, которая была успешно реализована в конце 70-х — начале 80-х Соловьем [39], Артемовым [1], Булосом [18] и др. Сегодня — это одно из самых плодотворных и впечатляющих приложений модальной логики.

Вторым крупным открытием, привлекшим широкое внимание к модальной логике, явилось найденное Ионссоном и Тарским [30] представление топологических булевых и других "модальных" алгебр в виде реляционных структур или шкал, как они теперь называются, и использование этих структур для построения семантики "возможных миров" (или семантики Крипке), формализовавшей старинную идею Лейбница о необходимости как истинности во всех возможных мирах. Это открытие дало импульс разработке трех основных теорий, на которых базируется все здание модальной логики: теории двойственности между шкалами и модальными алгебрами, теории полноты и теории определимости (см. [43]). Кроме того, возможность интерпретирования шкал как временных потоков, процессов вычислений или, скажем, процессов развития знаний познающих субъектов привела к разнообразным применениям модальной логики в теоретическом и практическом програм-

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

Одним из результатов вызванного этими открытиями ускоренного развития модальной логики вглубь и вширь явилось создание колоссального числа всевозможных модальных систем как естественного, так и искусственного происхождения. Это, в свою очередь, не могло не привести к разнообразным обобщениям. На рубеже 60-х и 70-х годов завершилось формирование абстрактного понятия (или, скорее, понятий) модальной логики и была явно поставлена задача разработки соответствующей общей теории (см., например, [23]). Систематические исследования близкого к модальным логикам класса расширений интуиционистского исчисления высказываний Int были инициированы еще раньше A.B. Кузнецовым, Т. Хосои и X. Оно.

Предмет и задачи модальной логики стали меняться. Ряд конкретных модальных систем дали начало более специальным дисциплинам, таким как логика доказуемости, временная, динамическая, эпистеми-ческая и т.п. логики. Общая же (или, по аналогии с алгеброй, универсальная) модальная логика сконцентрировалась на изучении больших семейств модальных систем. Ее главной целью стала разработка методов, пригодных для работы с логиками en masse. Создание теории двойственности между реляционной и алгебраической семантиками Йонссоном и Тарским [30], Леммоном [34], Эсакиа [13] и Гольдблатом [29], установление связи между модальными (и суперинтуиционистскими) логиками и многообразиями модальных (и псевдобулевых) алгебр Кузнецовым [2], Максимовой и Рыбаковым [5] и Блоком [16], а также между пропозициональным модальным языком и языком логики предикатов первого порядка Файном [24] и ван Бентемом [43] снабдили модальную логику теми математическими орудиями, которые были необходимы для выделения ее в самостоятельную и полноценную ветвь математической логики.

Современная модальная логика в таком широком понимании базируется в основном на теоретико-модельном (или теоретико-шкальном) и алгебраическом подходах. Связь между синтаксическими представлениями логик и их семантикой осуществляется общей теорией полноты, берущей начало с работ Була [19], Файна [23] и Салквиста [37]. Теоремы полноты обычно являются первым шагом в изучении разнообразных свойств логик. Классические примеры — исследование Максимовой [4] интерполяционного свойства или результаты о разрешимости, основан-

ные на полноте относительно "хороших" (скажем, конечных) шкал.

Стандартные семейства модальных логик обычно образуют решеточные структуры относительно теоретико-множественного включения. Это наблюдение дает начало исследованиям строения решеток логик, поднимающим вопросы об их коатомах (т.е. максимальных непротиворечивых логиках данного семейства), наличии бесконечно возрастающих цепей (т.е. существовании логик, не имеющих конечной аксиоматизации) и т.д. С алгебраической точки зрения решетка логик соответствует решетке подмногообразий некоторого фиксированного многообразия модальных алгебр, что открывает возможность использования методов и результатов хорошо разработанной области универсальной алгебры. Удивительные связи между "геометрическими" свойствами модальных формул, полнотой, аксиоматизируемостью и неразложимыми элементами решетки модальных логик были обнаружены Янковым [15], Блоком [17] и Раутенбергом [36].

Еще одним важным направлением современных исследований, возникающим только тогда, когда мы имеем дело с классами логик, является решение алгоритмической проблемы распознавания свойств (конечно аксиоматизируемых) логик. Существование неразрешимых исчислений (построенных Томасоном [41] и Шехтманом [10]), казалось бы, по аналогии с теоремой Райса-Успенского должно вести к неразрешимости нетривиальных свойств логик. Однако эта аналогия здесь не срабатывает. В решетке нормальных расширений Я4 разрешимыми оказываются, например, табличность и интерполяционное свойство, как было доказано Максимовой [3, 4]. Но большинство интересных свойств — разрешимость, финитная аппроксимируемость, полнота по Крипке, дизъюнктивное свойство и многие другие — все же неразрешимы. Техника получения такого рода отрицательных результатов разработана Томасоном [42] и Чагровым [9, 60].

Томасон [42] доказал неразрешимость полноты по Крипке сначала в классе полимодальных логик, а затем перенес этот результат на унимодальные логики путем погружения первых во вторые. Теория погружения и переноса вообще становится довольно мощным техническим средством в модальной логике, позволяя в ряде случаев сводить исследование новых типов логик к уже хорошо изученным. Наиболее известным примером такого рода сведения является погружение Орлова-Геделя интуиционистской логики и ее расширений в расширения Э4, применявшееся Дамметом и Леммоном [20], Максимовой и Рыбаковым

[5], Блоком [16] и Эсакиа [14], а также его обобщения на некоторые модальные логики с интуиционистской базой, построенные Фишер Серви [26] и Шехтманом [11]. Другой впечатляющий пример — недавние результаты Крахта и Вольтера [33] о сохранении свойств унимодальных логик при их независимом объединении в полимодальные.

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

Как уже отмечалось выше, уровень наших знаний о модальных логиках в значительной мере определяется имеющейся информацией об устройстве их шкал (или алгебр). Изучал некоторую решетку логик С и желая иметь в каком-то смысле универсальное средство для работы с ними, мы заинтересованы в нахождении единого описания (т.е. в одном и том же языке и с использованием одних и тех же понятий) "геометрии и топологии" их шкал. Если С — решетка расширений некой логики Ьо, то перед нами встает фундаментальная проблема характеризации класса всех тех шкал для Ьо, в которых общезначима (или опровергается) произвольно заданная модальная формула.

Целью работы является

• решение проблемы характеризации для модальных формул в классе транзитивных шкал с действительными мирами, т.е. для решетки Ех1К4 квазинормальных расширений базисной системы К4;

• разработка (на основе построенного в результате теоретико-модельного языка) методов доказательства разрешимости, финитной аппроксимируемости, сильной полноты, элементарности и других важных свойств логик из ЕхЖ4;

• исследование подрешетки логик, которые характеризуются классами шкал, замкнутыми относительно взятия (конфинальных) под-шкал;

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

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

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

Теоретическая и практическая ценность. Работа носит теоретический характер. Ее результаты и разработанные методы могут найти приложения в других областях неклассической логики, универсальной алгебре и теории моделей. Особый интерес представляет их использование для анализа модальных языков представления знаний в системах искусственного интеллекта (например, с целью доказательства разрешимости модальных логик описания понятий) и для построения алгоритмов анализа поведения программ с помощью временной логики. С другой стороны, работа открывает новое направление в рамках самой модальной логики — исследование проблемы характеризации в различных классах шкал.

Апробация. По результатам диссертации делались доклады на Всесоюзных и Всероссийских конференциях по математической логике (Тбилиси, 1982, пленарный доклад; Новосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990; Казань, 1992), на международной конференции РСТ'87 (Казань, 1987), на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), на международной конференции по алгебре (Новосибирск, 1989), на логических коллоквиумах Европейской Ассоциации символической логики (Берлин, 1989; Вежпрем, 1992; Киль, 1993; Клермон-Ферран, 1994), на логической конференции в Болгарии (София, 1990), на 4-ой Азиатской логической конференции (Токио, 1990), на международной конференции в центре Банаха (Варшава, 1991, приглашённый доклад), на конференциях по математической

логике в Японии (Ниигата, 1994; Сендай 1996; Каназава, 1996; Киото, 1997, все — приглашённые доклады), на Международном конгрессе по логике, методологии и философии науки (Флоренция, 1995), на международной конференции РОЫЛ (Чиба, 1996, приглашённый доклад), на конференции Ассоциации символической логики (Сан Диего, Калифорния, 1997). Приглашенные лекции были прочитаны в университетах Хиросимы (1990), Амстердама (1992, 1993, краткий курс о канонических формулах, 1997), Берлина (1992, 1994, 1995, 1997), Токио (1994), Милана (1996, краткий курс "Метод канонических формул"), Каназавы (1996), Нагойи (1997), Лейпцига (1997) и Аахена (1997). Результаты докладывались на научных семинарах Московского, Новосибирского, Иркутского и Киевского университетов.

Публикации. Основные результаты диссертации опубликованы в работах [46] - [75]; большая их часть вошла в монографию [63].

Структура и объём работы. Диссертация состоит из введения и четырех глав, разбитых на 22 параграфа. Объем работы — 251 страницы. Библиография — 172 наименование.

СОДЕРЖАНИЕ РАБОТЫ

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

Следует отметить, что эта проблема в столь общей формулировке явно никогда не ставилась и не решалась. Причина, по всей видимости, заключалась в отсутствии подходящего универсального языка для описалия "геометрических и топологических" свойств шкал. Традиционный первопорядковый подход достиг своего апогея в теореме Сал-квиста [37], давшей алгоритм построения формул первого порядка с равенством и предикатом достижимости, характеризующих строение шкал Крипке для большого, но все-таки ограниченного класса модальных формул. Многие важные пропозициональные модальные и интуиционистские формулы (например, аксиомы Лёба, Гжегорчика, Скотта) вообще не имеют первопорядковых эквивалентов на шкалах, не говоря

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

• разработка универсального теоретико-модельного языка, достаточного для характеризации (обобщенных) транзитивных шкал, опровергающих данную формулу в данной точке, а также создание его синтаксического аналога — языка канонических формул (см. параграфы 2.1 - 2.3).

Грубо говоря, каждая модальная каноническая формула J.) стро-

ится по конечной корневой шкале 5 = (W, R) и некоторому множеству 2) ее антицепей, называемых закрытыми областями, так чтобы шкала i25 опровергала 3D, ±) в том и только том случае, когда существует подредукция1 (или частичный р-морфизм) / из © на которая является конфиналъной в том смысле, что каждая точка, достижимая (по R) из области определения dorn/ подредукции /, либо "видит" dorn/, либо сама принадлежит dorn/ — символически dom/t С dom/4, — и удовлетворяет условию закрытых областей

(CDC) -ах € dom/t-dom/ 3D £ 33 /(art) = t>t

(т.е. никакая точка из dom/f—dorn/ не может "видеть" только прообразы всех точек из какой-либо закрытой области, их последователей и ничего больше).

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

S4.1 = S4 ф □ Ор ООр = S4 ф а((°Э, 0, ±),

где © — двухэлементный сгусток). А с другой стороны, в параграфе 2.3

• доказана теорема аксиоматической полноты, согласно которой каждая модальная формула может быть эффективно представлена в виде дедуктивно эквивалентного ей (т.е. аксиоматизирующего то

1Редукция — это реляционный аналог взятия подалгебры.

же самое расширение К4) конечного множества канонических формул.

Аналогичный результат установлен и для интуиционистского случая; интуиционистские канонические формулы обозначаются через /3(5,2), ±). Таким образом,

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

Частными случаями канонических формул оказываются хорошо известные интуиционистские характеристические формулы Янкова [15] и модальные шкальные формулы (frame formulas) Файна [22]; они дедуктивно эквивалентны формулам вида /3(5^, S", _L) иа(У,Э",±), соответственно, где 2)" — множество всех антицепей в Другой частный случай — подшкальные (subframe) формулы Файна [25], аксиоматизирующие в точности те нормальные расширения К4, которые характеризуются классами шкал, замкнутыми относительно образования подшкал. Однако множества формул Янкова и Файна аксиоматически полными не являются.

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

Традиционный метод доказательства разрешимости неклассических логик — это установление финитной аппроксимируемости (т.е. полноты относительно множества конечных шкал) и конечной аксиоматизируемости. Исследование этих свойств начинается в параграфе 3.1, где

• доказано, что финитно аппроксимируемы все нормальные модальные логики, канонические аксиомы которых не содержат закрытых областей (т.е. имеют вид а^,0, ±)).

Это достаточное условие охватывает почти все стандартные модальные логики, все расширения S4.3, уже упоминавшиеся подшкальные

логики Файна, все нормальные расширения S4 булевыми комбинациями модальностей и множество других интересных логик. Класс CST нормальных модальных логик с каноническими аксиомами вида а (5,0, J_) вообще оказывается замечательным во многих отношениях. В параграфах 3.1 и 3.2

• показано, что CST — полная подрешетка решетки NExtK4 нормальных расширений К4, а класс SJ- подшкальных логик — полная подрешетка CSJ-;

• построена континуальная антицепь подшкальных логик, что дает отрицательный ответ на известный вопрос о числе и разрешимости логик из «SJF (см. [25, 31]);

• дана теоретико-модельная характеризация CST: логика принадлежит CSJ- тогда и только тогда, когда она характеризуется классом шкал, замкнутым относительно образования конфинальных подшкал;

• вычислена верхняя (по порядку не уменьшаемая в общем случае) оценка — — размера минимальной шкалы, отделяющей формулу ip ^ Loi логики L £ CSJ- (здесь 1(<р) — число подформул

у);

• доказан критерий элементарности, каноничности и сильной полноты по Крипке логик из CSJ7.2

Эти результаты переносятся (с помощью доказываемых в работе теорем сохранения, которые обсуждаются чуть позже) на интуиционистский случай, где семейства CST и S F допускают не только теоретико-модельную, но и чисто синтаксическую характеризацию. А именно, в параграфе 3.2

• показано, что суперинтуиционистская логика аксиоматизируема импликативными формулами (или формулами, не содержащими дизъюнкции) тогда и только тогда, когда она характеризуется классом шкал, замкнутым относительно взятия подшкал (соответственно, конфинальных подшкал);

2Продолжая исследования в этом направлении, Вольтер [45] обобщил некоторые из упомянутых здесь результатов на класс минимальных временных расширений логик из CSF.

• установлено, что число суперинтуиционистских логик с имплика-тивными аксиомами континуально;

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

В параграфе 3.4 мы выходим за пределы решетки CST и обнаруживаем множество на удивление простых (благодаря языку канонических формул) примеров логик, не являющихся финитно аппроксимируемыми. Из новых результатов здесь можно отметить следующие:

• найден пример финитно не аппроксимируемого расщепления (splitting) решеток NExtK4 и NExtK4.3, что дает отрицательный ответ на давно стоявший вопрос (финитно не аппроксимируемые объединения расщеплений были построены Янковым [15] и Крах-том [32]);

• дан пример финитно не аппроксимируемой салквистовой логики, содержащей S4 (до этого подобный пример был известен только над К).

В параграфах 3.5 и 3.6 разработаны два новых метода доказательства финитной аппроксимируемости логик, канонические аксиомы которых могут содержать закрытые области, и

• получено несколько сильных достаточных условий финитной аппроксимируемости, накладываемых на вид канонических аксиом.

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

• доказана финитная аппроксимируемость всех нормальных расширений К4 принципами редукции модальностей4;

• доказана финитная аппроксимируемость всех нормальных расширений S4 конечным числом формул от одной переменной.

3Этот результат был независимо получен Шимурой [38], который также использовал метод канонических формул.

4 Принцип редукции модальностей — это формула вида Мр —f Np, где М v. N — цепочки (возможно пустые) □ и О.

Можно ли обобщить первый из этих результатов на класс всех нормальных логик, пока не известно. А вот второй результат оказывается принципиально не улучшаемым. Над К4 даже константные формулы могут аксиоматизировать финитно не аппроксимируемые логики, а над Я4 имеется построенная Шехтманом [12] финитно не аппроксимируемая логика с бесконечным числом аксиом от одной переменной. В параграфе 3.6

• показано, что имеется бесконечно возрастающая цепь логик из МЕх1Б4 с аксиомами от одной переменной и что число таких логик — континуум.

Использование метода канонических формул позволяет достигнуть значительного прогресса в развитии методов доказательства разрешимости при отсутствии свойства финитной аппроксимируемости и даже полноты по Крипке. В модальной логике существовал лишь один (несинтаксический) способ получения такого рода результатов — основанный на теореме Рабина о дереве метод редукций, предложенный Габба-ем [27] и примененный им для нескольких конкретных систем. В интуиционистском случае Соболеву [7] удалось воспользоваться некоторыми результатами теории автоматов для (довольно сложного) доказательства разрешимости конечно аксиоматизируемых тесных суперинтуиционистских логик конечной ширины. В основе методов, предложенных в данной работе, лежат теоремы о полноте относительно классов достаточно "хороших и прозрачных", хотя и бесконечных шкал, проверка общезначимости канонических формул в которых может быть выполнена за конечное время. Этим способом в параграфе 3.3

• доказана разрешимость всех конечно аксиоматизируемых квазинормальных расширений К4 каноническими формулами без закрытых областей (эти логики, вообще говоря, не являются полными по Крипке),

а в параграфе 3.7

• установлена разрешимость всех конечно аксиоматизируемых нормальных модальных логик, содержащих К4.3, что является существенным усилением известной теоремы Була-Файна [19, 21].5

5 Развивая предложенную в диссертации технику, Вольтер [44] недавно обобщил этот результат на линейные временные логики. Упомянутый выше результат Соболева также легко получается этой техникой.

Хотя модальные и суперинтуиционистские логики рассматриваются в работе параллельно, "настоящие" доказательства и построения проводятся лишь для модального случая. На суперинтуиционистские логики результаты, как правило, переносятся с помощью теории погружений, систематические исследования в которой были начаты Максимовой и Рыбаковым [5], Блоком [16] и Эсакиа [14]. Метод канонических формул позволяет представить эту теорию в очень наглядной и компактной форме, фактически превращая ее в мощный конвейер по переносу результатов с модального случая на интуиционистский и обратно. В параграфе 2.6

• получено описание устройства шкал для наименьшего модального напарника данной суперинтуиционистской логики;

• найден алгоритм, строящий по конечной аксиоматизации логики из NExtS4 аксиоматизацию ее суперинтуиционистского фрагмента;

• исследовано сохранение наиболее важных свойств логик при переходе от модальной логики к ее суперинтуиционистскому фрагменту и от суперинтуиционистской логики к ее наименьшему и наибольшему модальным напарникам; в частности, доказано сохранение разрешимости при всех этих переходах, сохранение полноты по Крипке (а также сильной полноты и каноничности) при переходе к наименьшему напарнику, что дало решение высказанной в 1959 году гипотезе Даммета-Леммона [20], несохранение независимой аксиоматизируемости при переходе к суперинтуиционистскому фрагменту.

В отличие от нормального случая, где логика Гжегорчика Grz оказывается наибольшим напарником интуиционистской логики и где имеет место теорема Блока-Эсакиа об изоморфизме, существуют, как показал Чагров [8], собственные квазинормальные расширения Grz, имеющие Int своим фрагментом. В параграфе 2.7 изучаются квазинормальные модальные логики, в которые Int погружается переводом Орлова-Геделя. В частности, с помощью метода канонических формул

• получено описание всех квазинормальных напарников Int из ExtS4;

• доказано, что среди них имеется наибольший, и изучены его основные свойства (так, он разрешим, финитно не аппроксимируем, обладает дизъюнктивным свойством и полон по Холдену);

• показано, что в квазинормальном случае теорема Блока-Эсакиа места не имеет.

Значительное внимание в последнее время стали привлекать модальные логики не на классической, а на интуиционистской (или, более общо, суперинтуиционистской) базе. Такие логики возникают из разных источников и имеют разные области приложений. Среди них — философия, основания математики, информатика. Модальности добавляются к интуиционистской логике в рамках изучения "новых интуиционистских связок" и для моделирования монадического фрагмента интуиционистской логики предикатов. Однако в отличие от классической модальной логики, интуиционистские модальные системы изучались до сих пор "по-штучно" с использованием их индивидуальных особенностей. Причина, очевидно, заключалась в том, что интуиционистские логики даже с одним модальным оператором гораздо ближе к бимодальным, чем к унимодальным классическим логикам, и только несколько последних лет принесли достаточно общие результаты в полимодальной логике.

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

• развивается теория двойственности между интуиционистскими модальными алгебрами и шкалами,

в параграфе 4.2

• разрабатывается теория погружений; в частности, доказывается аналог теоремы Блока-Эсакиа, согласно которому решетка интуиционистских модальных логик изоморфна некоторому главному фильтру решетки классических полимодальных логик, а также несколько теорем сохранения

и, наконец, в параграфе 4.3

• устанавливается несколько общих результатов о финитной аппроксимируемости и разрешимости интуиционистских модальных логик.

Литература

[1] С.Н. Артемов. Модальные логики доказуемости для расширений арифметики // Семиотика и информатика. 1978-1979. Т. 12. С. 43-46.

[2] A.B. Кузнецов. Некоторые свойства структуры многообразий псевдобулевых алгебр // XI Всесоюзный алгебраический коллоквиум: резюме сообщений и докладов. Кишинёв, 1971. С. 255-256.

[3] JI.JI. Максимова. Предтабличные расширения логики S4 Льюиса // Алгебра и логика. 1975. Т. 14. С. 28-55.

[4] JI.JI. Максимова. Интерполяционные теоремы в модальных логиках и амальгамируемые многообразия топобулевых алгебр // Алгебра и логика. 1979. Т. 18. С. 556-586.

[5] JI.JI. Максимова, В.В. Рыбаков. О решётке нормальных модальных логик // Алгебра и логика. 1974. Т. 13. С. 188-216.

[6] И.Е. Орлов. Исчисление совместности высказываний // Математический сборник. 1928. Т. 35. С. 263-286.

[7] С.К. Соболев. О конечномерных суперинтуиционистских логиках // Известия АН СССР. Сер. матем. 1977. Т. 41. С. 963986.

[8] A.B. Чагров Многообразия логических матриц // Алгебра и логика. 1985. Т. 24. С. 426-489.

[9] A.B. Чагров. Неразрешимые свойства расширений логики доказуемости И Алгебра и логика. 1990. Т. 29. С. 350-367, 613-623.

[10] В.Б. Шехтман. Неразрешимое суперинтуиционистское исчисление Ц Доклады АН СССР. 1978. Т. 240. С. 549-553.

[11] В.Б. Шехтман. Семантика Крипке для пропозициональных логик с интуиционистской базой // Модальные и временные логики. ИФ АН СССР. 1979. С. 108-112.

[12] В.Б. Шехтман. Топологические модели пропозициональных логик // Семиотика и информатика. 1980. Вып.15. С. 74-98.

[13] JT.J1. Эсакиа. О топологических моделях Крипке // Доклады АН СССР. 1974. Т. 214. С. 298-301.

[14] J1.JI. Эсакиа. К теории модальных и суперинтуиционистских систем // Логический вывод. М., Наука, 1979, с. 147-172.

[15] В.А. Янков. Построение последовательности сильно независимых суперинтуиционистских исчислений // Доклады АН СССР. 1968. Т. 181. С. 33-34.

[16] W.J. Blok. Varieties of interior algebras. PhD thesis, University of Amsterdam, 1976.

[17] W.J. Blok. On the degree of incompleteness in modal logics and the covering relation in the lattice of modal logics.

Technical Report 78-07, Department of Mathematics, University of Amsterdam, 1978.

[18] G. Boolos. The unprovability of consistency: an essay in modal logic. Cambridge University Press, 1979.

[19] R.A. Bull. That all normal extensions of S4.3 have the finite model property // Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 1966. V. 12. P. 341-344.

[20] M.A.E. Dummett, E.J. Lemmon. Modal logics between S4 and S5 II Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 1959. V. 5. P. 250-264.

[21] K. Fine. The logics containing S4.3 // Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 1971. V. 17. P. 371-376.

[22] K. Fine. An ascending chain of S4 logics // Theoria. 1974. V. 40. P. 110-116.

[23] K. Fine. Logics containing K4. Part I // Journal of Symbolic Logic. 1974. V. 39. P. 31-42.

[24] K. Fine. Some connections between elementary and modal logic // Proceedings of the Third Scandinavian Logic Symposium. North-Holland, Amsterdam, 1975, pages 15-31.

[25] K. Fine. Logics containing K4. Part II // Journal of Symbolic Logic. 1985. Y. 50. P. 619-651.

[26] G. Fischer Servi. On modal logics with an intuitionistic base // Studia Logica. 1977. V. 36. P. 141-149.

[27] D.M. Gabbay. On decidable, finitely axiomatizable modal and tense logics without the finite model property. I, II // Israel Journal of Mathematics. 1971. V. 10. P. 478-495, 496-503.

[28] k. gödel. Eine Interpretation des intuitionistischen Aussagenkalküls // Ergebnisse eines mathematischen Kolloquiums. 1933. V. 4. P. 39-40.

[29] R.I. Goldblatt. Metamathematics of modal logic. Part I// Reports on Mathematical Logic. 1976. V. 6. P. 41-78, V.7. P. 21-52.

[30] B. jönsson, A. Tarski. Boolean algebras with operators // American Journal of Mathematics. 1951. V. 73. No. 4. P. 891-939.

[31] M. Kracht. Internal definability and completeness in modal logic. PhD thesis, Freie Universität Berlin, 1991.

[32] M. kracht. Splittings and the finite model property // Journal of Symbolic Logic. 1993. V. 58. P. 139-157.

[33] M. Kracht, F. Wolter. Properties of independently axiomatizable bimodal logics // Journal of Symbolic Logic. 1991. V. 56. P. 14691485.

[34] E.J. Lemmon. Algebraic semantics for modal logic. I, II // Journal of Symbolic Logic. 1966. V. 31. P. 46-65, 191-218.

[35] J.C.C. McKinsey, A. Tarski. The algebra of topology // Annals of Mathematics. 1944. V. 45. P. 141-191.

[36] W. Rautenberg. Klassische und nichtklassische Aussagenlogik. Vieweg, Braunschweig-Wiesbaden, 1979.

[37] H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic // Proceedings of the Third Scandinavian Logic Symposium. North-Holland, Amsterdam, 1975, pages 110-143.

[38] t. shimura. Kripke completeness of some intermediate predicate logics with the axiom of constant domain and a variant of canonical formulas // Studia Logica. 1993. V. 52. P. 23-40.

[39] R. solovay. Provability interpretations of modal logic // Israel Journal of Mathematics. 1976. V. 25. P. 287-304.

[40] M.H. Stone. Application of the theory of Boolean rings to general topology // Transactions of the American Mathematical Society. 1937. V. 41. P. 321-364.

[41] s.k. thomason. The logical consequence relation of propositional tense logic // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1975. V. 21. P. 29-40.

[42] S.K. thomason. Undecidability of the completeness problem of modal logic // Universal Algebra and Applications, Banach Center Publications. PNW-Polish Scientific Publishers, Warsaw. 1982. V. 9. P. 341-345.

[43] J. van benthem. Modal logic and classical logic. Bibliopolis, Napoli, 1983.

[44] f. wolter. Properties of tense logics // Mathematical Logic Quarterly. 1996. V. 42. P. 481-500.

[45] F. wolter. Completeness and decidability of tense logics closely related to logics above K4 // Journal of Symbolic Logic. 1997. V. 62. P. 131-158.

РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

[46] Ф. Вольтер, M.B. Захарьящев. Об отношении между интуиционистскими и классическими модальными логиками // Алгебра и логика. 1997. Т. 36. С. 121-155.

[47] M.B. Захарьящев. Некоторые классы промежуточных логик. Препринт Ин. прикл. матем. им. M.B. Келдыша АН СССР. N 160. 1981 г.

[48] M.B. Захарьящев. О промежуточных логиках // Доклады АН СССР. 1983. Т. 27. С. 274-277.

[49] M.B. Захарьящев. Нормальные модальные логики, содержащие S4 // Доклады АН СССР. 1984. Т. 29. С. 252-255.

[50] М.В. Захарьящев. О дизъюнктивном свойстве суперинтуиционистских и модальных логик // Математические заметки. 1987. Т. 42. С. 729-738.

[51] М.В. Захарьящев. Синтаксис и семантика модальных логик, содержащих S4 И Алгебра и логика. 1988. Т. 27. С. 659-689.

[52] М.В. Захарьящев. Модальные напарники суперинтуиционистских логик: синтаксис, семантика и теоремы сохранения // Математический сборник. 1989. Т. 180. С. 1415-1427.

[53] М.В. Захарьящев. Синтаксис и семантика суперинтуиционистских логик // Алгебра и логика. 1989. Т. 28. С. 402-429.

[54] М.В. Захарьящев, A.B. Чагров. Неразрешимость дизъюнктивного свойства суперинтуиционистских исчислений. Препринт Ин. прикл. матем. им. М.В. Келдыша АН СССР. N 57. 1989 г.

[55] М.В. Захарьящев, A.B. Чагров. Неразрешимость свойства полноты по Холдену модальных исчислений. Препринт Ин. прикл. матем. им. М.В. Келдыша АН СССР. N 82. 1990 г.

[56] G. Bezhanishvili. М. Zakharyaschev. Logics over MIPC // In Т. Shimura, editor, Sequent Calculus and Kripke Semantics, pp.8695, RIMS, Kyoto University, No. 1021, 1997.

[57] A. Chagrov, M. Zakharyaschev. On Hallden-completeness of intermediate and modal logics // Bulletin of the Section of Logic. 1990. V. 19. No. 1. P. 21-24.

[58] A. Chagrov, M. Zakharyaschev. The disjunction property of intermediate propositional logics // Studia Logica. 1991. V. 50. No. 2. P. 189-216.

[59] A. Chagrov, M. Zakharyaschev. Modal companions of intermediate propositional logics // Studia Logica. 1992. V. 51. No. 1. P. 49-82.

[60] A. Chagrov, M. Zakharyaschev. The undecidability of the disjunction property of propositional logics and other related problems // Journal of Symbolic Logic. 1993. V. 58. No. 3. P. 967-1002.

[61] A. Chagrov, M. Zakharyaschev. On the independent axiomati-zability of modal and intermediate logics // Journal of Logic and Computation 1995. V. 5. No. 3. P. 287-302.

[62] A. Chagrov, M. Zakharyaschev. Sahlqvist formulas are not so elementary even above S4. // Logic Colloquium '92 (L. Csirmaz, D.M. Gabbay and M. de Rijke, eds). CSLI, Stanford, 1995, pp. 61-73.

[63] A. Chagrov, M. Zakharyaschev. Modal Logic. Clarendon Press, Oxford, 1997, 605 p.

[64] Y. Suzuki, F. Wolter, M. Zakharyaschev. Speaking about transitive frames in propositional languages. Preprint IS-RR-97-0002F (ISSN 0918-7553), School of Information Science, Japan Advanced Institute of Science and Technology, Hokuriku, 1997. (To appear in the Journal of Logic, Language and Information.)

[65] M. Zakharyaschev. Theorem proving in intermediate and modal logics // Lecture Notes in Computer Science. (O.B. Lupanov, editor) 1987. V. 278. P. 492-496.

[66] M. Zakharyaschev. Canonical formulas for K4. Part I: Basic results /1 Journal of Symbolic Logic. 1992. V. 57. P. 1377-1402.

[67] M. Zakharyaschev. Intermediate logics with disjunction free axioms are canonical // IGPL Newsletter. 1992. V. 1. P. 7-8.

[68] M. Zakharyaschev. A sufficient condition for the finite model property of modal logics above K4 // Bulletin of the IGPL. 1993. V. 1. P. 13-21.

[69] M. Zakharyaschev, A new solution to a problem of Hosoi and Ono /1 Notre Dame Journal of Formal Logic. 1994. V. 35. P. 450-457.

[70] M. Zakharyaschev. Canonical formulas for K4. Part II: Cofinal subframe logics // Journal of Symbolic Logic. 1996. V. 61. P. 421449.

[71] M. Zakharyaschev. Canonical formulas for K4. Part III: The finite model property // Journal of Symbolic Logic. 1997. V. 62. P. 950975.

[72] M. Zakharyaschev. The greatest extension of S4 into which intuitio-nistic logic is embeddable // Studia Logica. 1997. V. 59. P. 345-358.

[73] M. Zakharyaschev. Canonical formulas for modal and superintui-tionistic logics: a short outline. In M. de Rijke, editor, Advances in Intensional Logic, pp.195-248, Kluwer Academic Publishers, 1997.

[74] M. Zakharyaschev, A. Alekseev. All finitely axiomatizable normal extensions of K4.3 are decidable // Mathematical Logic Quarterly. 1995. V. 41. P. 15-23.

[75] M. Zakharyaschev, F. Wolter, A. Chagrov. Advanced modal logic. Preprint IS-RR-96-0027F (ISSN 0918-7553), School of Information Science, Japan Advanced Institute of Science and Technology, Hokuriku, 1996. (To appear as a chapter in the Handbook of Philosophical Logic, D. Gabbay and F. Guenthner (eds.), 2nd edition, Reidel, Dordrecht, 1998.)

I

' JT X ¿

. О С С ИИ/

ирезиАьун

(решение " íb ШЬ^

присудил ученую ст* . i

шриуилиэ^ iUQ и Ma íV^-r НаВДА£пик ym~ .. JC Р

РОССИЙСКАЯ АКАДЕМИЯ НАУК ИНСТИТУТ ПРИКЛАДНОЙ МАТЕМАТИКИ имени М.В. КЕЛДЫША

на правах рукописи

ЗАХАРЬЯЩЕВ Михаил Викторович

МЕТОД КАНОНИЧЕСКИХ ФОРМУЛ И ЕГО ПРИМЕНЕНИЯ В МОДАЛЬНОЙ ЛОГИКЕ

Специальность 01.01.06 — математическая логика, алгебра и теория чисел

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

Москва 1998

Содержание

Введение 3

1 Начальные сведения 19

1.1 Решетки Extlnt и Ext К 4........................................................19

1.2 Семантика........................................................................26

1.3 Семантика перевода Орлова-Геделя............................................34

1.4 Точки конечной глубины в рафинированных шкалах........................40

1.5 Универсальные шкалы конечного ранга ......................................47

2 Канонические формулы 53

2.1 Подредукция......................................................................55

2.2 Конфинальная подредукция и условие закрытых областей..................65

2.3 Характеризация опровергающих шкал........ ........................75

2.4 Канонические формулы для К4 и Int..........................................87

2.5 Квазинормальные канонические формулы....... ...........100

2.6 Модальные напарники си-логик................................................105

2.7 Наибольший напарник Int в ExtS4............................................118

3 Применения метода канонических формул 129

3.1 Cs- и csf-логики. I................................................................129

3.2 Cs- и csf-логики. II................................................................142

3.3 Квазинормальные sf- и csf-логики..............................................157

3.4 За пределами СБТ................................................................163

3.5 Метод вставки....................................................................168

3.6 Метод удаления..................................................................181

3.7 Логики, содержащие К4.3......................................................196

4 Модальные логики с интуиционистской базой 203

4.1 Начала теории двойственности.........................203

4.2 Начала теории погружений...........................215

4.3 Начала теории полноты.............................226

Библиография 235

Введение

Модальная логика — одна из наиболее динамично развивающихся ветвей математической логики, нашедшая многочисленные приложения в основаниях математики, философии, информатике, лингвистике, искусственном интеллекте и других областях. Начавшись, казалось бы, с не очень-то обоснованных систем Льюиса [115, 116], которые вряд ли бы заметили в серьезных математических кругах, своим нынешним положением она обязана, прежде всего, двум открытиям.

Во-первых, прочитав льюисовский оператор □ (некой абстрактной) необходимости как "доказуемо", Орлов [30]1 и Гедель [99] дали классическую интерпретацию интуиционистской пропозициональной логики Int посредством погружения ее в модальную систему "доказуемости", которая к тому же оказалась эквивалентной льюисовской S4. Это открытие, с одной стороны, стимулировало установление связи модальной и интуиционистской логик с топологией и алгеброй в виде построения Стоуном [147], а также Маккинси и Тарским [122, 123] топологической и алгебраической семантик для S4 и Int. А с другой стороны, оно продемонстрировало возможность использования модальной логики в основаниях математики для анализа феномена доказуемости в формальных системах, которая была успешно реализована в конце 70-х — начале 80-х Соловьем [143], Артемовым [1], Булосом [66] и др. Сегодня — это одно из самых плодотворных и впечатляющих приложений модальной логики. "Если исследования в области модальной логики или семантические понятия, развитые для ее изучения, и нуждались когда-либо в научном обосновании, теорема Соловья и ее доказательство их предоставляют," —

ХК сожалению, эта работа Орлова, опубликованная за 5 лет до заметки Геделя [99], оставалась незамеченной вплоть до 80-х годов.

писал Булос [68].

Вторым крупным открытием, привлекшим широкое внимание к модальной логике, явилось найденное Йонссоном и Тарским [106] представление топологических булевых и других "модальных" алгебр в виде реляционных структур или шкал, как они теперь называются, и использование этих структур для построения семантики "возможных миров" в работах Кангера [107], Хинтикки [104] и Крипке [111], формализовавшей старинную идею Лейбница о необходимости как истинности во всех возможных мирах. Это открытие дало импульс построению "трех столпов ..., на которых покоится все здание модальной логики — ... всепроникающей теории полноты, ... теории соответствия или определимости и ... теории двойственности между шкалами Крипке и модальными алгебрами" (ван Бентем [154]).

С другой стороны, возможность интерпретирования шкал как временных потоков, процессов вычислений или, скажем, процессов развития знаний познающих субъектов привела к разнообразным применениям модальной логики в теоретическом и практическом программировании, искусственном интеллекте, философии, лингвистике и ряде других областей. "Этот подход имел огромное влияние не только на логику необходимости и возможности, но также и на другие области. В частности, его идеи были использованы с целью разработки формализмов для описания многих других видов структур и процессов в информатике, давших предмету (модальной логике — М.З.) приложения, которые, вероятно, удивили бы как самих его создателей, так и их клеветников", — пишут Барвайс и Мосс [59].

Одним из результатов вызванного этими открытиями ускоренного развития модальной логики вглубь и вширь явилось создание колоссального числа всевозможных систем как естественного, так и искусственного происхождения.2 Это, в свою очередь, не могло не привести к разнообразным обобщениям. На рубеже 60-х и 70-х годов завершилось формирование абстрактного понятия (или, скорее, понятий) модальной логики

2Интересно, что одна из самых знаменитых систем модальной логики — логика доказуемости Геделя-Леба СЬ — была введена сначала Сегербергом [138] как "искусственная" система под именем К4Л¥.

и была явно поставлена задача разработки соответствующей общей теории. "Последние работы по модальной логике," — писал Файн [90], — "содержат два больших пробела: нам недостает общих результатов и результатов отрицательного характера. Обычно показывается, что та или иная логика обладает таким-то и таким-то свойством, однако очень мало известно о протяженности и границах этого свойства. Таким образом, имеются многочисленные результаты о полноте, разрешимости, финитной аппроксимируемости, компактности и т.д., но очень мало общих или отрицательных результатов." Систематические исследования близкого к модальным логикам класса расширений интуиционистского исчисления высказываний были инициированы еще раньше А.В. Кузнецовым, Т. Хосои и X. Оно.

Предмет и задачи модальной логики стали меняться. Ряд конкретных модальных систем дали начало более специальным дисциплинам, таким как логика доказуемости, временная, деонтическая, динамическая, квантовая, эпистемическая и т.п. логики. Общая же (или, по аналогии с алгеброй, универсальная) модальная логика сконцентрировалась на изучении больших семейств модальных систем. Ее главной целью стала разработка методов, пригодных для работы с логиками en masse. Создание теории двойственности между реляционной и алгебраической семантиками Ионссоном и Тар-ским [106], Леммоном [114], Эсакиа [51] и Гольдблатом [100], установление связи между модальными (и суперинтуиционистскими) логиками и многообразиями модальных (и псевдобулевых) алгебр Кузнецовым [17], Максимовой и Рыбаковым [28] и Блоком [62], а также между пропозициональным модальным языком и языком логики предикатов первого или более высокого порядка Файном [91] и ван Бентемом [153] снабдили модальную логику теми математическими орудиями, которые были необходимы для выделения ее в самостоятельную и полноценную ветвь математической логики.

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

берущей начало с работ Була [70], Файна [90], Салквиста [136], Гольдблата и Томасо-на [101]. Теоремы полноты обычно являются первым шагом в изучении разнообразных свойств логик, особенно если эти свойства имеют алгебраические или семантические эквиваленты. Классические примеры — исследование Максимовой [26] интерполяционного свойства нормальных модальных логик, содержащих S4, или результаты о разрешимости, основанные на полноте относительно "хороших" (скажем, конечных) шкал. Теория полноты предоставляет также средства для аксиоматизации логик, задаваемых классами шкал, и дает критерии аксиоматизируемости таких классов.

Стандартные семейства модальных логик обычно образуют решеточные структуры относительно теоретико-множественного включения. Это наблюдение дает начало исследованиям строения решеток логик, поднимающим вопросы об их коатомах (т.е. максимальных непротиворечивых логиках данного семейства), наличии бесконечно возрастающих цепей (т.е. существовании логик, не имеющих конечной аксиоматизации) и т.д. С алгебраической точки зрения решетка логик соответствует решетке подмногообразий некоторого фиксированного многообразия модальных алгебр, что открывает возможность использования методов и результатов хорошо разработанной области универсальной алгебры. Удивительные связи между "геометрическими" свойствами модальных формул, полнотой, аксиоматизируемостью и неразложимыми элементами решетки модальных логик были обнаружены Янковым [54, 55], Блоком [63, 64] и Раутенбергом [133].

Еще одним важным направлением современных исследований, возникающим только тогда, когда мы имеем дело с классами логик, является решение алгоритмической проблемы распознавания свойств (конечно аксиоматизируемых) логик. Существование неразрешимых исчислений (построенных Томасоном [150] и Шехтманом [46]), казалось бы, по аналогии с теоремой Райса-Успенского должно вести к неразрешимости нетривиальных свойств логик. Однако эта аналогия здесь не срабатывает. В решетке нормальных расширений S4 разрешимыми оказываются, например, табличность и интерполяционное свойство Крейга, как было доказано Максимовой [24, 26]. Но большинство интересных свойств все же неразрешимы. Техника получения такого рода отрицатель-

ных результатов разработана Томасоном [151] и Чагровым [40, 76].

Томасон [151] доказал неразрешимость полноты по Крипке сначала в классе всех полимодальных логик, а затем перенес этот результат на унимодальные логики путем погружения первых во вторые. Теория погружения и переноса вообще становится довольно мощным техническим средством в модальной логике, позволяя в ряде случаев сводить исследование новых типов логик к уже хорошо изученным. Пожалуй, наиболее известным примером такого рода сведения является погружение Орлова-Геделя интуиционистской логики и ее расширений в расширения Б4, применявшееся Дамметом и Леммоном [83], Максимовой и Рыбаковым [28], Блоком [62] и Эсакиа [53], а также его обобщения на некоторые модальные логики с интуиционистской базой, построенные Фишер Серви [93] и Шехтманом [48]. Другой впечатляющий пример — недавние результаты Крахта и Вольтера [110] о сохранении свойств унимодальных логик при их независимом объединении в полимодальные.

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

Как уже отмечалось выше, уровень наших знаний о модальных логиках в значительной мере определяется имеющейся информацией об устройстве их шкал (или алгебр). Изучая некоторую решетку логик С и желая иметь в каком-то смысле универсальное средство для работы с ними, мы заинтересованы в нахождении единого описания (т.е. в одном и том же языке и с использованием одних и тех же понятий) "геометрии и топологии" их шкал. Если С — решетка расширений некой логики Ь0, а чаще всего это именно так, то перед нами встает фундаментальная проблема харак-теризации класса всех тех шкал для Ьо, в которых общезначима (или опровергается) произвольно заданная модальная формула.

Целью диссертационной работы является: • решение проблемы характеризации для модальных формул в классе транзитив-

ных шкал с действительными мирами, т.е. для решетки Ех1;К4 квазинормальных расширений базисной системы К4;

• разработка (на основе построенного в результате теоретико-модельного языка) методов доказательства разрешимости, финитной аппроксимируемости, сильной полноты, элементарности и других важных свойств логик из Ех<;К4;

• исследование подрешетки логик, которые характеризуются классами шкал, замкнутыми относительно взятия (конфинальных) подшкал;

• развитие теории погружений суперинтуиционистских логик в расширения Б4, а также модальных логик на интуиционистской базе в классические полимодальные логики, и применение полученных теорем сохранения для изучения свойств этих логик.

Следует отметить, что проблема характеризации в столь общей формулировке явно никогда не ставилась и не решалась. Причина, по всей видимости, заключалась в отсутствии подходящего универсального языка для описания "геометрических и топологических" свойств шкал. Традиционный первопорядковый подход достиг своего апогея в теореме Салквиста [136], давшей алгоритм построения формул первого порядка с равенством и предикатом достижимости, характеризующих строение шкал Крипке для большого, но все-таки ограниченного класса модальных формул. Многие важные пропозициональные модальные и интуиционистские формулы (например, аксиомы Лёба, Гжегорчика, Скотта) вообще не имеют первопорядковых эквивалентов на шкалах, не говоря уже о том, что ввиду существования неполных по Крипке логик (см. [89, 45]) требуется описывать обобщенные шкалы, а не только шкалы Крипке. Одним из наиболее важных результатов данной работы является

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

Грубо говоря, каждая модальная каноническая формула S, _L) строится по конечной корневой шкале J = (W,R) и некоторому множеству D ее антицепей, называемых закрытыми областями, так чтобы шкала <3 опровергала Э, _L) в том и только том случае, когда существует подредукция3 (или частичный р-морфизм) / из © на 3\ которая является конфиналъной в том смысле, что каждая точка, достижимая (по R) из области определения dorn/ подредукции /, либо "видит" dorn/, либо сама принадлежит dorn/, — символически dom/t С dom/J, — и удовлетворяет условию закрытых областей

(CDC) ->3х G dom/t-dom/ 3t> е ® /(st) = *>t

(т.е. никакая точка из dom/f—dorn/ не может "видеть" только прообразы всех точек из какой-либо закрытой области, их последователей и ничего больше).

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

S4.1 = S4 ф ПОр ОПр = S4 е а((оо), 0, ±), где (оо) — двухэлементный сгусток). А с другой стороны, в параграфе 2.3

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

Аналогичный результат установлен и для интуиционистского случая; интуиционистские канонические формулы обозначаются посредством £>,_!_). Канонические представления многих стандартных модальных и суперинтуиционистских логик можно найти в таблицах на стр. 94 и 97. Таким образом,

3Редукция — реляционный аналог взятия подалгебры.

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

Частными случаями канонических формул являются хорошо известные интуиционистские характеристические формулы Янкова [54, 55] и модальные шкальные формулы (frame formulas) Файна [88]; они дедуктивно эквивалентны формулам вида /З^,®", _L) и «(З, £)", _L), соответственно, где £>" — множество всех антицепей в Другой частный случай — подшкальные (subframe) формулы Файна [92], аксиоматизирующие в точности те нормальные расширения К4, которые характеризуются классами шкал, замкнутыми относительно образования подшкал. Однако множества формул Янкова и Файна аксиомат�