Модальные логики топологических пространств

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

Теория модальных логик — быстро развивающийся и сравнительно новый раздел математической логики. Изучение логических свойств модальностей было начато еще в античные времена, но на протяжении многих столетий велось лишь в рамках гуманитарных дисциплин (главным образом, философии и лингвистики). Первые модально-логические исчисления были сформулированы только в начале 20-го века (К. Льюис, 1918), а осознание теории модальностей с математической точки зрения началось лишь в 40-е — 50-е гг., благодаря работам А. Тарского, Дж. Маккинси, Б. Йонссона, С. Крипке и др.

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

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

Топологическая (окрестностная) семантика модальных логик.

В данной диссертации модальные логики рассматриваются как формальные теории топологических пространств. Изучение топологических пространств средствами математической логики началось достаточно давно. Сама идея построения простого исчисления, в котором можно доказывать топологические теоремы, по существу, принадлежит К. Куратовскому [KURATOWSKJ 1922] (хотя похожая система аксиом предлагалась ранее Риссом [RIESZ 1909]). Проблема создания «топологической теории моделей», аналогичной теории моделей классической логики первого порядка была поставлена А. Робинсоном [ROBINSON 1973]. Принципиальная трудность здесь состоит в том, что топологические структуры невозможно определить в языке первого порядка, поскольку для задания топологического пространства нужно говорить и о точках, и о множествах точек. Таким образом, приходится использовать фрагменты 5 логики второго порядка, что существенно осложняет задачу. Тем не менее, в этом направлении ведутся активные исследования [FLUM, ZIEGLER 1980], [FLUM 1995]. Достоинством теорий второго порядка является богатство их выразительных возможностей, а недостатком — алгоритмическая неразрешимость (и во многих случаях, неперечислимость).

Альтернативный подход к теориям топологических пространств предлагает модальная логика. Хотя при этом получаются более слабые исчисления, они, как правило, оказываются разрешимыми. Теория моделей для этих исчислений активно разрабатывалась во 2-й половине 20-го века.

Использование модальной логики мотивируется непосредственно аксиоматикой Куратовского, которая, в терминах булевых операций и операции внутренности (i) аксиомы топологического пространства имеет вид: А1. ?(YnZ') = iYniZ А2. iYciiY A3. i YcY A4. i 1 = 1.

Здесь 1 — все пространствоY, Z — его подмножества).

Аксиомы А1-А4 можно рассматривать как абстрактные алгебраические тождествабулева алгебра с дополнительной операцией, удовлетворяющей этим тождествам, называется топобулевой. Каждому топологическому пространству X отвечает топобулева алгебра МА (^), состоящая из всех его подмножеств с булевскими операциями и операцией внутренности.

С тождествами в сигнатуре топобулевых алгебр (n, u,-, 0, l, i) естественно связаны формулы в языке модальной логики: тождество t = г, где t, г — топобулевы термы с переменными х-|, Х2,., можно переписать в виде формулы логики высказываний, если заменить символы операций и константы п, и, 0, 1, i соответственно на логические связки и константы л (и), v (или), -1 (не), 1 (ложь), Т (истина),? (необходимо), знак равенства — на связку ~ (эквивалентно), а предметные переменные xi, Х2,. — на пропозициональные переменные p-j, р2,.

Обратно, каждой модальной формуле, А отвечает тождество tA = 1, где tAсоответствующий топобулев терм.

Модальная формула, А называется общезначимой в топобулевой алгебре Д если тождество tA = 1 истинно в j6. Множество всех модальных формул, общезначимых в Д называется модальной логикой алгебры il 6.

Модальная формула, А общезначима в топологическом пространстве X, если она общезначима в алгебре Ык{%). Модальной логикой пространства % (обозначение: ~{Х)) называется модальная логика алгебры МА (Л^), т. е. множество всех модальных формул, общезначимых в Xмодальной логикой класса пространств С (обозначение: L (C)) называется множество всех модальных формул, общезначимых во всех пространствах из С.

Если аксиомы А1-А4 записать в виде модальных формул, то получатся схемы аксиом известного модального исчисления S4: А1 D (AaB)~DAADB А2'. DAoDDA A3'. DAz>A A4'. ?Т~Т В постулаты S4 входят также схемы аксиом классической логики,.

А, А: эВ правило modus ponens д.

А~ В и правило эквивалентной замены? А~? В.

Под логикой S4 обычно понимается множество теорем этого исчисления1. Вообще (нормальной) (моно)модальной логикой принято называть множество модальных формул, содержащее все классические тавтологии и все формулы вида А1', A4' и замкнутое относительно правил подстановки, эквивалентной замены и modus ponensS4- логики — это модальные логики, содержащие S4.

Классическим результатом является следующая теорема Линденбаума об алгебраической полноте:

34-логики суть в точности модальные логики топобулевых алгебр2.

Связь между аксиомами Куратовского и логикой S4 была обнаружена независимо в [STONE 1937], [TARSKI 1938], [TANG 1938]. В этих работах была доказана теорема о топологической полноте:

S4 есть модальная логика класса всех топологивческих пространств.

Систематическое исследование топобулевых алгебр было начато в [MCKJNSEY, TARSKI 1944]3. В этой области одной из центральных тем стало исследование.

1 В дальнейшем будет использоваться несколько другая, эквивалентная аксиоматизация S4.

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

3 Точнее говоря, в [MCKINSEY, TARSKI1944] изучается эквивалентное понятие — алгебры замыкания (closure algebras). 7 многообразий, или, двойственным образом, исследование эквациональных теорий топобулевых алгебр. Из теоремы Линденбаума следует, что эти теории в точности соответствуют 34-логикам.

Для дальнейшего изучения топологической семантики полезным оказалось эквивалентное определение общезначимости модальной формулы в терминах «возможных миров», предложенное в [MONTAGUE 1968], [SCOTT 1970]. Напомним это определение.

Оценкой в топологическом пространстве % называется отображение ср, сопоставляющее с каждой пропозициональной переменнной подмножество X. Оценка продолжается на все модальные формулы по следующему правилу: ф (-, А)"#-<�р (А), ф (АлВ)=ф (А)пф (В), ф (AvB) =ф (А)иф (В), ф (ША)=Чф (А).

Формула, А называется истинной в точке w пространства X при оценке ф, если шеф (А). (Сокращенно это обозначается через wNA.) Таким образом, общезначимость модальной формулы в X равносильна ее истинности во во всех точках при всех оценках.

Правило продолжения оценки эквивалентно индуктивному определению истинности в точке: wN-i A^wJ^AwNAaBo (wNA и wl=B) — wNAvB"(wNA rnmwNB) — wNGA о {у I у NA} -окрестность w.

Если представлять себе точки пространства X как «возможные миры» или как наблюдателей, которые оценивают формулы как истинные или ложные, то данное определение достаточно естественно. В частности: w признаетiA, если он не признает А, w признает DA, если, А признается истинной в окрестности w, т. е. если все наблюдатели, достаточно близкие к w, признают А.

Таким образом, в этой семантике «необходимость» интерпретируется как «локальная истинность» [SCOTT 1970].

Заметим еще, что окрестностную семантику можно определить и для модальных логик, не являющихся расширениями S4. В этом случае вместо топологических пространств используются окрестности ые шкалы, удовлетворяющие аксиомам А1, A4, но не обязательно А2 и A3, а вместо топобулевых алгебр — модальные алгебры. 8.

Реляционная семантика модальных логик.

Реляционная семантика (или семантика Крипке), ставшая основным инструментом в модальной логике, была введена неявно в [J6NSSON, TARSKI 1951], [J6NSS0N, TARSKI 1952], [DUMMETT, LEMMON 1959] и явно — в работах С. Крипке [KRIPKE 1959], [KRIPKE 1963]. Ее можно рассматривать как частный случай окрестностной семантики.

Напомним, что шкалой Крипке (Kripke frame) называется непустое множество (множество возможных миров) с заданным на нем бинарным отношением (отношением достижимости). Если (W, R) — шкала Крипке, то на множестве всех подмножеств W имеется операция iX = {x|Vy (xRy=i>yе X)}.

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

В случае шкал Крипке определение истинности в точке (для формулы вида ПА) приобретает вид: wNDA о Vv (wRv =>vHA), т. е. необходимость здесь понимается как истинность во всех достижимых мирах.

Модальной логикой шкалы Крипке (W, R) называется модальная логика соответствующего топологического пространства N (W, R).

Суперинтуиционистские логики.

С топобулевыми алгебрами тесно связаны алгебры Хейтинга (или псевдобулевы) [TARSKI 1938], [MCKINSEY, TARSKI 1946]. Алгебру Хейтинга можно определить как дистрибутивную решетку с нулем и единицей и относительным псевдодополнением («импликацией»): a-«b = U{x|anx^b}. Эти алгебры получаются также из полных топобулевых алгебр как алгебры открытых элементов (т.е. элементов вида ix).

Система тождеств, задающая многообразие алгебр Хейтинга, фактически является системой аксиом интуиционистской логики высказываний, а эквациональные теории алгебр Хейтинга соответствуют суперинтуиционистским логикам, т. е. расширениям интуиционистской логики. Суперинтуиционистские логики связаны с модальными посредством перевода Гёделя — Тарского. Он ставит в.

4 Топология пространства N (W, R) называется также правой топологией, индуцированной отношением R (см. [БУРБАКИ 1968]). 9 соответствие каждой интуиционистской формуле, А модальную формулу т (А) по следующим правилам:

• т (А) = А, если, А — пропозициональная переменнаяt (-iA) = D-i7(A) — t (AvB) = t (A)vt (B) — т (АлВ) = т (А)лт (В) — t (A-*B) = D (t (A)z>t (B)).

Благодаря этому переводу, суперинтуиционистские логики оказываются фрагментами модальных 34-логик и потому могут рассматриваться в контексте общей теории модальных логик. Точнее говоря, каждой модальной логике Л отвечает суперинтуиционистский фрагмент, состоящий из всех интуиционистских формул, переводы которых принадлежат Л. Обратно, у каждой суперинтуиционистской логики L имеются модальные напарники, т. е. модальные логики с суперинтуиционистским фрагментом Lсреди модальных напарников имеется наибольший r (L) и наименьший o (L).

Наибольшим модальным напарником интуиционистской логики является логика Гжегорчика Grz, получающаяся из S4 добавлением схемы аксиом? (?(А=эйА)эА)эА.

Известно, что множество всех расширений Grz, упорядоченное по включению, изоморфно множеству всех суперинтуиционистских логик посредством отображения, а (теорема Блока — Эсакиасм. [ЧАГРОВ, ЗАХАРЬЯЩЕВ 1997]).

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

Общая проблематика теории модальных и суперинтуиционистских логик.

В последние десятилетия исследования модальных и суперинтуиционистских логик и соответствующих им алгебр проводились по следующим основным направлениям:

• исследование решеток многообразий и решеток соответствующих логик;

• описание свободных алгебр в различных многообразиях и доказательство теорем о представлении;

• построение различных семантик неклассических логик и исследование их свойств;

• построение адекватных интерпретаций логик в других логиках и теориях;

• исследование алгоритмических проблем;

• исследование квазимногоообразий и допустимых правил вывода;

• исследование конкретных свойств логик и семейств логик: компактности, свойства Лёвенгейма — Сколема, конечной аксиоматизируемости, интерполяционного свойства, дизъюнктивного свойства и проч.

Во всех этих направлениях был достигнут существенный прогресс. Перечислим здесь лишь некоторые важные результаты, полученные в нашей стране: в работах [МАКСИМОВА, РЫБАКОВ 1974], [МАКСИМОВА 1975], [ЭСАКИА 1979], [ЭСАКИА 1979а] изучалась решетка модальных логик и связь между решетками модальных и суперинтуиционистских логикв работах [МАКСИМОВА 1977], [МАКСИМОВА 1991] и др. были доказаны общие теоремы об интерполяционных свойствах суперинтуиционистских и модальных логикв работе [ШЕХТМАН 1978] была впервые построена неразрешимая конечно аксиоматизируемая суперинтуиционистская логика (и, как следствие — 34-логика с аналогичными свойствами) — позднее были найдены более простые примеры (см. [ЧАГРОВ, ЗАХАРЬЯЩЕВ 1997]) — в работе [ШЕХТМАН 1978а] было дано описание свободных топобулевых и гейтинговых алгебр конечного ранга5- в работах [РЫБАКОВ 1984], [РЫБАКОВ 1985], [РЫБАКОВ 1994] и др. была показана разрешимость допустимости правил для многих модальных и суперинтуиционистских логик (и, как следствие, — разрешимость универсальных теорий соответствующих свободных алгебр) — в работе [ЧАГРОВ 1994] была доказана неразрешимость для большинства известных свойств суперинтуиционистских и модальных исчисленийв работах [ЗАХАРЬЯЩЕВ 1989], [ЗАХАРЬЯЩЕВ 1996], [ЗАХАРЬЯЩЕВ 1997] был доказан ряд общих теорем о разрешимости модальных и суперинтуиционистских логик и о сохранении свойств при переходе от суперинтуиционистских логик к модальным.

Важнейшие результаты и общие методы теории модальных логик были систематизированы в недавно вышедшей монографии [ЧАГРОВ, ЗАХАРЬЯЩЕВ 1997].

Многомерные и пространственные модальные логики.

Наряду с исследованием общих свойств логик, в 70-е гг. в модальной логике возникло новое направление, изучающее модальные логики многомерных структур:

5 Результаты работ [ШЕХТМАН 1978] и [ШЕХТМАН 1978а] изложены в кандидатской диссертации автора [ШЕХТМАН 1984].

11 геометрических, топологических и реляционных. В моделях этих логик «возможные миры» понимаются как пространственные объекты (точки, прямые, регулярные области и проч.) или же как абстрактные «точки с координатами» .

Интенсивное развитие многомерных и пространственных логик вызвано их связями с целым рядом других областей:

• Классическая логика предикатов: изучение фрагментов логики предикатов первого порядка (в частности, в финитной области) и связанных с ними алгебраических структур — цилиндрических, полиадических и реляционных алгебр [MARX, VENEMA 1997], [VAN BENTHEM 1996].

• Неклассические логики предикатов: изучение фрагментов модальных и суперинтуиционистских предикатных логик, а также исследование семантик этих логик [СКВОРЦОВ, ШЕХТМАН 1993], [GABBAY, SHEHTMAN 1993], [WOLTER, ZAKHARYASCHEV 1999].

• Теоретическая информатика (Theoretical Computer Science): изучение логик систем переходов и алгебр процессовпостроение и исследование логик паралллельных вычислений [REIF, SISTLA 1985], [LADNER, REIF 1986], [DE RDKE 1993], [SPAAN 1993], [ARNOLD 1994], [VAN BENTHEM 1996].

• Теория искусственного интеллекта (Artificial Intelligence): создание логических основ систем представления знаний (динамические логики дескрипций) [BAADER, OHLBACH 1995], [WOLTER, ZAKHARYASCHEV 1998], [WOLTER, ZAKHARYASCHEV 1998a]- построение и использование логик геометрических и топологогических структур в задачах качественного анализа пространственной информации [BENNETT.

1996], [COHN, BENNETT, GOODAY, GOTTS 1998], [AIELLO, VAN BENTHEM 1999].

• Лингвистическая семантика: логический анализ временно-видовых и дейктических конструкций [AQVIST, GUNTHER 1978], [NISHIMURA 1980],.

• Математическая физика: построение и изучение временных логик для различных моделей пространства-времени [GOLDBLATT 1980], [ШЕХТМАН 1983], [RODRIGUEZ, ANGER 1993].

Хотя общая теория многомерных и пространственных модальных логик пока не создана, здесь уже получен ряд нетривиальных результатов. Например, активно исследовались произведения модальных логик: впервые в [ШЕХТМАН 1978b], [ШЕХТМАН 1987] и более глубоко в [GABBAY, SHEHTMAN 1998], [REYNOLDS, ZAKHARYASCHEV 1999], [WOLTER 1998], [MARX 1999], [KURUCZ 1999]. Проводилось также исследование модальных логик подмножеств действительной плоскости [ШЕХТМАН 1983], интервальных модальных логик [MARX, VENEMA.

1997], [NISHIMRA 1980], модальных логик проективных плоскостей [BALBIANI, FARINAS DEL CERRO, TINCHEV, VAKARELOV 1997]. К пространственной логике.

12 следует отнести и исследование модальных логик топологических пространствразнообразные подходы к этим логикам и прикладные их аспекты обсуждалются в [BENNETT, GOODAY, GOTTS 1998], [AIELLO, VAN BENTHEM 1999].

Основные результаты диссертации.

В настоящей диссертации модальные и суперинтуиционистские логики высказываний исследуются с точки зрения их топологической (окрестностной) семантики. При этом, как и в классической теории моделей, рассматриваются вопросы двух основных типов:

— построение логики, описывающей данный класс топологических пространств и исследование ее свойств;

— нахождение класса пространств, отвечающего данной логике.

В диссертации получены следующие основные результаты.

1. В классе расширений логики Гжегорчика найдены модальные логики, неполные в топологической семантике.

2. Доказана неэквивалентность топологической семантики и семантики Крипке для суперинтуиционистских логик.

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

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

5. Построены системы аксиом и доказана финитная аппроксимируемость деривационных логик для пространств Rn и для нульмерных плотных в себе подмножеств действительной прямой.

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

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

Опишем теперь результаты диссертации более подробно.