Введение к работе
Актуальность темы. Модальная логика — одна из наиболее динамично развивающихся ветвей математической логики, нашедшая многочисленные приложения в основаниях математики, философии, информатике, лингвистике, искусственном интеллекте и других областях. Начавшись, казалось бы, с не очень-то обоснованных систем Льюиса (1918, 1932), которые вряд ли бы заметили в серьезных математических кругах, своим нынешним положением она обязана, прежде всего, двум открытиям.
Во-первых, прочитав льюисовский оператор (некой абстрактной) необходимости как "доказуемо", Орлов [6] и Гёдель [28] дали классическую интерпретацию интуиционистской пропозициональной логики Int посредством погружения ее в модальную систему "доказуемости", которая к тому же оказалась эквивалентной льюисовской S4. Это открытие, с одной стороны, стимулировало установление связи модальной и интуиционистской логик с топологией и алгеброй в виде построения Стоуном [40], а также Маккинси и Тарским [35] топологической и алгебраической семантик для S4 и Int. А с другой стороны, оно продемонстрировало возможность использования модальной логики в основаниях математики для анализа феномена доказуемости в формальных системах, которая была успешно реализована в конце 70-х — начале 80-х Соловьем [39], Артемовым [1], Булосом [18] и др. Сегодня — это одно из самых плодотворных и впечатляющих приложений модальной логики.
Вторым крупным открытием, привлекшим широкое внимание к модальной логике, явилось найденное Йонссоном и Тарским [30] представление топологических булевых и других "модальных" алгебр в виде реляционных структур или шкал, как они теперь называются, и использование этих структур для построения семантики "возможных миров" (или семантики Крипке), формализовавшей старинную идею Лейбница о необходимости как истинности во всех возможных мирах. Это открытие дало импульс разработке трех основных теорий, на которых базируется все здание модальной логики: теории двойственности между шкалами и модальными алгебрами, теории полноты и теории определимости (см. [43]). Кроме того, возможность интерпретирования шкал как временных потоков, процессов вычислений или, скажем, процессов развития знаний познающих субъектов привела к разнообразным применениям модальной логики в теоретическом и практическом програм-
мировании, искусственном интеллекте, философии, лингвистике и ряде других областей.
Одним из результатов вызванного этими открытиями ускоренного развития модальной логики вглубь и вширь явилось создание колоссального числа всевозможных модальных систем как естественного, так и искусственного происхождения. Это, в свою очередь, не могло не привести к разнообразным обобщениям. На рубеже 60-х и 70-х годов завершилось формирование абстрактного понятия (или, скорее, понятий) модальной логики и была явно поставлена задача разработки соответствующей общей теории (см., например, [23]). Систематические исследования близкого к модальным логикам класса расширений интуиционистского исчисления высказываний Int были инициированы еще раньше А.В. Кузнецовым, Т. Хосои и X. Оно.
Предмет и задачи модальной логики стали меняться. Ряд конкретных модальных систем дали начало более специальным дисциплинам, таким как логика доказуемости, временная, динамическая, эпистеми-ческая и т.п. логики. Общая же (или, по аналогии с алгеброй, универсальная) модальная логика сконцентрировалась на изучении больших семейств модальных систем. Ее главной целью стала разработка методов, пригодных для работы с логиками en masse. Создание теории двойственности между реляционной и алгебраической семантиками Йонссоном и Тарским [30], Леммоном [34], Эсакиа [13] и Гольдблатом [29], установление связи между модальными (и суперинтуиционистскими) логиками и многообразиями модальных (и псевдобулевых) алгебр Кузнецовым [2], Максимовой и Рыбаковым [5] и Блоком [16], а также между пропозициональным модальным языком и языком логики предикатов первого порядка Файном [24] и ван Бентемом [43] снабдили модальную логику теми математическими орудиями, которые были необходимы для выделения ее в самостоятельную и полноценную ветвь математической логики.
Современная модальная логика в таком широком понимании базируется в основном на теоретико-модельном (или теоретико-шкальном) и алгебраическом подходах. Связь между синтаксическими представлениями логик и их семантикой осуществляется общей теорией полноты, берущей начало с работ Була [19], Файна [23] и Салквиста [37]. Теоремы полноты обычно являются первым шагом в изучении разнообразных свойств логик. Классические примеры — исследование Максимовой [4] интерполяционного свойства или результаты о разрешимости, основан-
ные на полноте относительно "хороших" (скажем, конечных) шкал.
Стандартные семейства модальных логик обычно образуют решеточные структуры относительно теоретико-множественного включения. Это наблюдение дает начало исследованиям строения решеток логик, поднимающим вопросы об их коатомах (т.е. максимальных непротиворечивых логиках данного семейства), наличии бесконечно возрастающих цепей (т.е. существовании логик, не имеющих конечной аксиоматизации) и т.д. С алгебраической точки зрения решетка логик соответствует решетке подмногообразий некоторого фиксированного многообразия модальных алгебр, что открывает возможность использования методов и результатов хорошо разработанной области универсальной алгебры. Удивительные связи между "геометрическими" свойствами модальных формул, полнотой, аксиоматизируемостью и неразложимыми элементами решетки модальных логик были обнаружены Янковым [15], Блоком [17] и Раутенбергом [36].
Еще одним важным направлением современных исследований, возникающим только тогда, когда мы имеем дело с классами логик, является решение алгоритмической проблемы распознавания свойств (конечно аксиоматизируемых) логик. Существование неразрешимых исчислений (построенных Томасоном [41] и Шехтманом [10]), казалось бы, по аналогии с теоремой Райса-Успенского должно вести к неразрешимости нетривиальных свойств логик. Однако эта аналогия здесь не срабатывает. В решетке нормальных расширений S4 разрешимыми оказываются, например, табличность и интерполяционное свойство, как было доказано Максимовой [3, 4]. Но большинство интересных свойств — разрешимость, финитная аппроксимируемость, полнота по Крипке, дизъюнктивное свойство и многие другие — все же неразрешимы. Техника получения такого рода отрицательных результатов разработана Томасоном [42] и Чагровым [9, 60].
Томасон [42] доказал неразрешимость полноты по Крипке сначала в классе полимодальных логик, а затем перенес этот результат на унимодальные логики путем погружения первых во вторые. Теория погружения и переноса вообще становится довольно мощным техническим средством в модальной логике, позволяя в ряде случаев сводить исследование новых типов логик к уже хорошо изученным. Наиболее известным примером такого рода сведения является погружение Орлова-Геделя интуиционистской логики и ее расширений в расширения S4, применявшееся Дамметом и Леммоном [20], Максимовой и Рыбаковым
[5], Блоком [16] и Эсакиа [14], а также его обобщения на некоторые модальные логики с интуиционистской базой, построенные Фишер Серви [26] и Шехтманом [11]. Другой впечатляющий пример — недавние результаты Крахта и Вольтера [33] о сохранении свойств унимодальных логик при их независимом объединении в полимодальные.
Таковы основные направления исследований в современной (математической) модальной логике. В той или иной степени данная диссертационная работа затрагивает каждое из них, однако в основе разрабатываемого в ней подхода лежит решение одной фундаментальной проблемы, относящейся к общей теории полноты.
Как уже отмечалось выше, уровень наших знаний о модальных логиках в значительной мере определяется имеющейся информацией об устройстве их шкал (или алгебр). Изучая некоторую решетку логик С и желая иметь в каком-то смысле универсальное средство для работы с ними, мы заинтересованы в нахождении единого описания (т.е. в одном и том же языке и с использованием одних и тех же понятий) "геометрии и топологии" их шкал. Если С — решетка расширений некой логики L0) то перед нами встает фундаментальная проблема характеризации класса всех тех шкал для Lq, в которых общезначима (или опровергается) произвольно заданная модальная формула.
Целью работы является
решение проблемы характеризации для модальных формул в классе транзитивных шкал с действительными мирами, т.е. для решетки ExtK4 квазинормальных расширений базисной системы К4;
разработка (на основе построенного в результате теоретико-модельного языка) методов доказательства разрешимости, финитной аппроксимируемости, сильной полноты, элементарности и других важных свойств логик из ExtK4;
исследование подрешетки логик, которые характеризуются классами шкал, замкнутыми относительно взятия (конфинальных) под-шкал;
развитие теории погружений суперинтуиционистских логик в расширения S4, а также модальных логик на интуиционистской базе в классические полимодальные логики, и применение полученных теорем сохранения для изучения свойств этих логик.
Методы исследования включают семантические методы теории модальных и суперинтуиционистских логик, а также методы универсальной алгебры, теории моделей классической логики первого порядка и теории алгоритмов.
Научная новизна. Все основные результаты диссертации — построение языка канонических формул, применение его для решения проблемы характеризации, разработка на этой основе методов доказательства полноты, разрешимости и других свойств, реализация этих методов для решения ряда открытых проблем теории модальных и суперинтуиционистских логик, развитие и применение теории погружений и переноса — являются новыми.
Теоретическая и практическая ценность. Работа носит теоретический характер. Ее результаты и разработанные методы могут найти приложения в других областях неклассической логики, универсальной алгебре и теории моделей. Особый интерес представляет их использование для анализа модальных языков представления знаний в системах искусственного интеллекта (например, с целью доказательства разрешимости модальных логик описания понятий) и для построения алгоритмов анализа поведения программ с помощью временной логики. С другой стороны, работа открывает новое направление в рамках самой модальной логики — исследование проблемы характеризации в различных классах шкал.
Апробация. По результатам диссертации делались доклады на Всесоюзных и Всероссийских конференциях по математической логике (Тбилиси, 1982, пленарный доклад; Новосибирск, 1984; Москва, 1986; Ленинград, 1988; Алма-Ата, 1990; Казань, 1992), на международной конференции FCT'87 (Казань, 1987), на X Всесоюзной конференции по логике, методологии и философии науки (Минск, 1990), на международной конференции по алгебре (Новосибирск, 1989), на логических коллоквиумах Европейской Ассоциации символической логики (Берлин, 1989; Вежпрем, 1992; Киль, 1993; Клермон-Ферран, 1994), на логической конференции в Болгарии (София, 1990), на 4-ой Азиатской логической конференции (Токио, 1990), на международной конференции в центре Банаха (Варшава, 1991, приглашённый доклад), на конференциях по математической
логике в Японии (Ниигата, 1994; Сендай 1996; Каназава, 1996; Киото, 1997, все — приглашённые доклады), на Международном конгрессе по логике, методологии и философии науки (Флоренция, 1995), на международной конференции FOLLI (Чиба, 1996, приглашённый доклад), на конференции Ассоциации символической логики (Сан Диего, Калифорния, 1997). Приглашенные лекции были прочитаны в университетах Хиросимы (1990), Амстердама (1992, 1993, краткий курс о канонических формулах, 1997), Берлина (1992, 1994, 1995, 1997), Токио (1994), Милана (1996, краткий курс "Метод канонических формул"), Каназавы (1996), Нагойи (1997), Лейпцига (1997) и Аахена (1997). Результаты докладывались на научных семинарах Московского, Новосибирского, Иркутского и Киевского университетов.
Публикации. Основные результаты диссертации опубликованы в работах [46] - [75]; большая их часть вошла в монографию [63].
Структура и объём работы. Диссертация состоит из введения и четырех глав, разбитых на 22 параграфа. Объем работы — 251 страницы. Библиография — 172 наименование.