Дискретно-непрерывная математика (стр. 64 )

К сожалению, в общем случае никакого эффективного критерия табличности не существует. Однако, если мы ограничимся доста­точно сильными логиками, например, классом нормальных расши­рений S4, то проблема табличности оказывается разрешимой. Опи­сание всех предтабличных логик в этом классе дано [Максимова 1975] (таковых оказалось 5). А еще ранее установила (1972), что в классе si-логик со­держится в точности три предтабличных логики, одна из которых есть логика Гёделя-Даммита Естественно, возникает вопрос о предтабличных расширениях логики Лукасевича Из работы [Beavers 1993] следует, что существует только одно предтабличное расширение Обозначим эту логику посредством (мы рассмотрим ее в разделе 10.6.1).

Значительное продвижение в исследовании предтабличных модальных логик было сделано в [Blok 1980]. Оказалось, например, что в нормальных расширениях модальной логики К4 имеется

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

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

8.4.3. Шкалы Крипке и принцип соответствия

Ввиду тесной связи между модальной логикой S4 и интуиционист­ской логикой Int, первоначальной семантикой для S4 и ее расши­рений была алгебраическая, которая уже систематически исследо­валась Дж. Мак-Кинси в 1941 г. Модальные алгебры для многих модальных систем были введены Е. Леммоном [Lemmon 1966]. Здесь особое место занимает работа [Jonsson and Tarski 1951]. Как отмечается в [Bull and Segerberg 1984], если бы эта работа по­лучила известность после ее публикации, то история модальной ло­гики была бы другой. В этой работе была расширена теорема пред­ставления Стоуна на булеву алгебру с операторами, при этом в явном виде введены шкалы как реляционные представления мо­дальных алгебр.

Одной из наиболее привлекательных черт семантики возмож­ных миров, получившей необычайно широкое признание, является обнаружение простой связи между существованием модальных ак­сиом и обычными свойствами отношения достижимости между мирами. Такая связь положена в основание теории соответствия: какие классы моделей (шкал) Крипке можно описать модальными формулами, какие - формулами классической логики первого по­рядка. В действительности, теория соответствия выросла из весьма простого наблюдения, сделанному в начале 70-х годов: Т-аксиома истинна на шкале Крипке т. т.т., когда R рефлексивно. Здесь «истинна на шкале» обозначает истинность во всех мирах при всех приписываниях значений пропозициональным перемен­ным. Аксиома 4 эквивалентна транзитивности, а аксиома В - симметричности. Отсюда логика К4 характеризуется классом всех транзитивных шкал, логика S4 — классом всех транзитивных и реф­лексивных шкал и логика S5 характеризуется отношением эквива­лентности на множестве миров W. Тогда модальная логика К назы­вается базисной и примечательна тем, что в семантике Крипке для модальных логик на отношение достижимости не накладывается никаких ограничений. Другими словами, множество формул логи­ки К общезначимо во всех шкалах Крипке. Что касается логики Гжегорчика Grz, то она характеризуется классом всех финитных частично-упорядоченных шкал, а логика доказуемости GL харак­теризуется транзитивными и ирефлексивными (т. е. строго-упорядочнными) шкалами и при этом не содержащими бесконеч­ных обрывающихся цепей.

В [Van Benthem 1984] приведена таблица соответствий для не­которых интересных формул. Вообще при таком подходе модаль­ная формула определяет ограничения на отношения достижимости в шкалах Крипке. Некоторые из этих ограничений являются перво-порядково определимыми, другие нет. Например, в этой же работе показано, что свойства шкал Крипке, определяемых аксиомой Лёба, не являются первопорядково определимыми.

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

Исследования в области модальной логики к началу XXI века естественным образом оказалась разбиты на два уровня (два слоя, два направления): пропозициональный мономодальный и предикатно-кванторный вместе с многомодальным. Основные достиже­ния в области пропозициональной модальной логики собраны в фундаментальной монографии [Chagrov and Zakharyaschev 1997] и большой обзорной статье [Zakharyaschev, Wolter and Chagrov 2001]. Прекрасным введением в первопорядковую модальную логику яв­ляется книга [Fitting and Mendelsohn 1998]. Рассматриваются тех­нические и философские аспекты квантификации и тождества. Представлены гильбертовские и табличные системы.

8.4.4. Отступление

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

Важнейшим этапом современных исследований является изу­чение решеточных свойств классов логик. Уже в статье [Scroggs 1951] впервые было рассмотрено семейство модальных логик, в данном случае нормальные расширения S5, в виде решетки.

В [Hosoi 1969] установлено, что множество всех si-логик, упо­рядоченное отношением включения, образует решеточную струк­туру, а на самом деле - алгебру Рейтинга. Так начался совершенно новый этап в развитии логики — изучение решеточных свойств не отдельной логики, а семейства логик и их классификации.

Аналогично обстоит дело с множеством собственных расши­рений Элементы этого множества будем называть sl-логиками. Р. Григолия [Григолия 1976] установил, что множество всех sl-логик образует алгебру Рейтинга. Независимо от Григолия этот ре­зультат был установлен также в [Kojnori 1981]. В [Beavers 1993] было продолжено изучение расширений в виде гейтинговой структуры.

Для S4 подобные исследования впервые были проведены в [Максимова и Рыбаков 1974].

( Конечно, возникает вопрос, почему решетка теорий является брауэровой? При­рода этого феномена скорее всего заключается в природе операции присоеди­нения следствий (замыкания), используемой А. Тарским при определении логи­ки. Эта операция является топологическим замыканием, а логики - замкнутые множества, в том числе si-логики и sl-логики. Остается вспомнить связь топобулевых алгебр, псевдобулевых алгебр (алгебр Рейтинга) и брауэровых алгебр: так, всякая псевдобулева (брауэрова) алгебра является алгеброй открытых (замкнутых) элементов подходящей топо-булевой алгебры; во всякой топобулевой алгебре совокупность открытых (замкнутых) элементов образует псевдобулеву (брауэрову) алгебру.)

Представление расширений логических систем в виде структу­рированных множеств (решеток) позволяет устанавливать погру­жающие операции между такими логическими объектами. Здесь мы уже имеем дело не с погружением одной логической системы в другую, а с погружением решетки одних логик в решетку других логик. Особо отметим теорему Блока-Эсакиа: независимо В. Блок [Blok 1976] и [Эсакиа 1979] (ранее заявлено в тезисах конференции 1974 года) доказали изоморфизм решеток si-логик и нормальных расширений Grz. Такие погружения интересны не только с теоретической точки зрения, но могут служить важным инструментом для редуцирования одного класса логик к другому, уже хорошо изученному.

В обзоре [Bull and Segerberg 1984] лишь отмечается, что все нормальные логики образуют дистрибутивную решетку относи­тельно теоретико-множественного включения, которая чрезвычай­но сложна. В книге [Chagrov and Zakhajyaschev 1997] содержится глава 4 под названием «От логик к классам логик», где оговорено,

что классы расширений модальных логик рассматриваются как ре­шетки. Здесь явно обозначена тенденция к изучению не отдельных логик, а огромных (зачастую, континуальных) классов логик и раз­витие общих методов исследования этих классов. Наконец, обзор [Zakharyaschev, Wolter and Chagrov 2001] начинается с представле­ния решетки расширений логики К. Такой подход, отмечается ав­торами в предисловии, дает возможность использовать мощный технический аппарат, который позволяет ставить вопросы типа «что является

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