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

• Шехтман, Валентин Борисович
• доктор физико-математических наук
• 1999

Оглавление диссертации доктор физико-математических наук Шехтман, Валентин Борисович

ВВЕДЕНИЕ.

ГЛАВА 1. ОСНОВНЫЕ ПОНЯТИЯ

1.1. Модальные и суперинтуционистские логики.

1.2. Модальные алгебры.

1.3. Окрестностные шкалы.

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

1.5. Морфизмы окрестностных шкал.

1.6. Морфизмы шкал и моделей Крипке.

1.7. Канонические модели.

1.8. Фильтрации.

ГЛАВА 2. ОКРЕСТНОСТНАЯ ПОЛНОТА И ПОЛНОТА ПО КРИПКЕ

2.1. Пополнения.

2.2. Вспомогательные формулы и шкала Файна.

2.3. Пространства Гжегорчика.

2.4. Окрестностно неполное конечно аксиоматизируемое расширение логики Гжегорчика.

2.5. Окрестностно неполное расширение логики Гжегорчика с одной переменной.

2.6. Пространство У.

2.7. Относительно неполное суперинтуиционистское исчисление с двумя переменными.

ГЛАВА 3. СИЛЬНАЯ ОКРЕСТНОСТНАЯ ПОЛНОТА

3.1. Предварительные замечания.

3.2. Ультрабукеты шкал Крипке.

3.3. 8-К-полные модальные логики.

3.4. З-И-полные суперинтуиционистские логики.

3.5. Ультрабукеты топологических пространств.

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

4.1. Постановка задачи.

4.2. Логики и модели.

4.3. Логика 84иС; ее финитная аппроксимируемость.

4.4. с-р-морфизмы.

4.5. Окрестностная полнота S4UC.

ГЛАВА 5. ДЕРИВАЦИОННЫЕ МОДАЛЬНЫЕ ЛОГИКИ

5.1. Операция деривации и ее свойства.

5.2. Деривационные модальные логики.

5.3. Минимальная деривационная логика.

5.4. К4 и D4 как деривационные логики.

5.5. d-р-морфизмы: усиление леммы Маккинси - Тарского.

5.6. К4 и D4 как деривационнные логики нульмерных пространств,

5.7. Обобщенные формулы Куратовского.

5.8. Полнота по Крипке логик D4KUn.

5.9. Финитная аппроксимируемость логик D4KUn.

5.10. Подходящие шкалы.

5.11. D4KLH как деривационная логика.

5.12. D4KU2 как деривационная логика.

ГЛАВА 6. ВРЕМЕННЫЕ ЛОГИКИ С ОПЕРАТОРОМ ЛОКАЛЬНОЙ ИСТИННОСТИ

6.1. Постановка задачи.

6.2. Постулаты и полнота по Крипке для логик FPdI, FParj

6.3. Фильтрации.

6.4. Полнота FParj относительно линий времени.

6.5. Теоремы о полноте для других FPd-логик.

Введение диссертации (часть автореферата) на тему «Модальные логики топологических пространств»

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

Теория модальных логик - быстро развивающийся и сравнительно новый раздел математической логики. Изучение логических свойств модальностей было начато еще в античные времена, но на протяжении многих столетий велось лишь в рамках гуманитарных дисциплин (главным образом, философии и лингвистики). Первые модально-логические исчисления были сформулированы только в начале 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 ponens; S4- логики - это модальные логики, содержащие 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^A; wNAaBo(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.

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

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

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

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

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

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

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

10

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

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

Во всех этих направлениях был достигнут существенный прогресс. Перечислим здесь лишь некоторые важные результаты, полученные в нашей стране: в работах [МАКСИМОВА, РЫБАКОВ 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].

• Лингвистическая семантика: логический анализ временно-видовых и дейктических конструкций [ÁQVIST, GÜNTHER 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, FARIÑAS DEL CERRO, TINCHEV, VAKARELOV 1997]. К пространственной логике

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

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

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

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

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

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

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

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

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

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

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

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

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

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