Содержание к диссертации
Введение
1 Логики а-пространств 11
1.1 Основные понятия 11
1.1.1 Топологические пространства Ершова 11
1.1.2 Модальные логики и шкалы Крипке 14
1.1.3 Канонические модели 17
1.1.4 Финитно модельное свойство и фильтрации . 18
1.2 Теорема о корректности 19
1.3 Логические исчисления LD и I/ 25
1.4 Канонические модели для LD и I 29
1.5 Разрешимость исчислений LD, I/ 35
2 Модальная логика строго линейно упорядоченных шкал 46
2.1 Постановка задачи 46
2.2 Lf и структура канонической модели 49
2.3 Теорема о полноте 52
2.4 Финитная аппроксимируемость Lf 62
3 Временная логика строго линейно упорядоченных пространств 66
3.1 Теорема о корректности 66
3.2 Канонические модели для L*f и L*fo 69
3.3 Теорема о полноте 70
3.4 Финитная аппроксимируемость L*f, L*fo 86
- Модальные логики и шкалы Крипке
- Канонические модели для LD и I
- Lf и структура канонической модели
- Канонические модели для L*f и L*fo
Введение к работе
Теория неклассических логик - одна из важных областей современной логики. Особую роль играют модальные и временные логики. Хотя изучение логических свойств модальностей началось ещё во времена Аристотеля, теория модальных логик является сравнительно новым разделом математической логики: в начале 20-го века К.Льюис сформулировал первые модальные исчисления, а стремительный рост в этой области начался в 40-е - 50-е гг, благодаря работам С.Крипке, К.Льюиса,
Дж.МакКинси, Б.Ионссона, А.Тарского и др. Временная логика, как независимая область исследования, возникла благодаря работам Прайора [23].
Модальная логика по сравнению с классической логикой, отличается большим разнообразием синтаксиса и семантики: кроме обычных логических связок используются различные модальности типа необходимости и возможности. Этим можно объяснить широкое применение модальных и временных логик, например, в информатике, теории искус ственного интеллекта, математической лингвистике. Здесь можно упо мянуть различные работы, связанные с методами представления знаний [31], [17], логикой стрелок [30]. Теория временных логик также является особенно важной в связи с развитием параллельных вычислений (см.,например, [22]).
В последнее время неклассические логики широко применяются к изучению геометрических структур (например, модальные логики подмножеств действительной плоскости [28], интервальные времен ные логики [9]) и топологических пространств. Так, например, в [8] В.Б. Шехтманом в языке с оператором локальной и универсальной истинности построена система аксиом и доказана финитная аппроксимируемость логики произвольного связного, плотного в себе сепарабельного метрического пространства. Также в [8] построена система аксиом для логики рациональной прямой и логики класса всех линейных порядков в языке с временными операторами и операторм локальной истинности.
Применение модальной логики к изучению топологических пространств можно объяснить тем, что модальные логики высказываний можно исследовать с точки зрения их топологической (окрестностной) семантики. Топологическая интерпретация модальности была дана в работах Дж. МакКинси и А.Тарского [21], где была доказана топологическая полнота широко известной модальной логики S4, и позднее в [24]. В окрестностной семантике "необходимость" () интерпретируется как "локальная истинность" [24]: если рассматривать точки топологического пространства X как возможные миры, в которых формулы истинны или ложны, то формула ПА истинна в х Є X , если А истинна в некоторой окрестности мира х.
Кроме того, известно, что невозможно многие топологические структуры определить в языке первого порядка. Таким образом, возникает необходимость использовать язык второго порядка. Хотя при аксиоматизации топологических пространств в языке модальной логики строятся более слабые исчисления, они, как правило, являются разрешимыми.
В данной работе исследуются полимодальные логики, связанные с топологическими пространствами Ершова («-пространствами, /-пространствами, /о-пространствами). При этом рассматривается следующий вопрос: построение логики, описывающей данный класс топологических пространств, и исследование её свойств.
Понятие /-пространства было введено Ю.Л.Ершовым [2], [3], с целью развить теорию вычислимых функционалов. Кроме того, пространства Ершова можно рассматривать как топологический подход к теории областей Ершова-Скотта (domain theory), см. [13], которая является одним из важных разделов современной математики. Теория областей Ершова-Скотта возникла в 70-е гг. независимо в работах Ю.Л.Ершова ([12], [1]) и Д.Скотта [25]. Скоттом теория областей введена как теория программных языков и наиболее развилась в теоретической информатике. В [13] Ю.Л.Ершовым доказано, что введенное Д.Скоттом понятие 5-domain и понятие полного /о-пространства эквивалентны.
В данной работе модальные логики, связанные с пространтвами Ер шова, исследуются не только с точки зрения их топологической семантики, но и реляционной.
Реляционная семантика (или семантика Крипке) является основным инструментом в модальной логике. Реляционная семантика была введена неявно Б.Ионссоном и А.Тарским [29], Дамметтом и Леммоном [11], явно — в работах С.Крипке [18], [19], и использует понятие шкалы. Шкалой Крипке называется непустое множество (множество возможных миров) с заданным на нем бинарным отношением достижимости. Если (X, R) — шкала Крипке, то модальность можем связать с отношением R и понимать ее как истинность во всех достижимых мирах. Если мы рассматриваем временную логику, то с бинарным отношением R связываем две модальности: прошлого ( ) и будущего (). Тогда в случае шкал Крипке определение истинности в точке (для формул вида П Л, ОА) приобретает вид:
х \= и А = Vy{yRx = у (= А),
х \= ПА ==$ My{xRy == у \= А).
Заметим, что в данной работе используются как шкалы Крипке с одним бинарным отношением, так и с несколькими.
Цель работы — найти модальные и временные логики, которые характеризуют классы шкал, основанных на пространствах Ершова.
В диссертации использованы семантические методы неклассических логик, такие как, например, метод канонических моделей, метод фильтраций.
Все результаты диссертации являются новыми и снабжены подробными доказательствами.
Основные результаты диссертации:
1) Строятся полимодальные исчисления, корректные относительно шкал, основанных на а-пространствах. Доказывается разрешимость этих исчислений.
2) Введены классы строго линейно упорядоченных /-шкал и строго линейно упорядоченных /о-шкал. Найдено модальное исчисление, полное относительно этих классов. Доказано, что оно обладает финитно модельным свойством.
3) Построены два исчисления временной логики, одно из которых характеризует класс строго линейно упорядоченных /-шкал, другое — класс строго линейно упорядоченных /о-шкал. Доказана финитная аппроксимируемость этих исчислений.
Работа носит теоретический характер. Ее методы и результаты могут быть полезны специалистам в области неклассических логик Института Математики СО РАН, Московского, Новосибирского, Красноярского и др. госуниверситов.
Основные результаты, полученные в диссертации, докладывались на:
• заседаниях семинаров "Алгебра и логика" и "Нестандартные логики" кафедры алгебры и математической логики механико-математического
факультета НГУ,
• международной научной студенческой конференции "Студент и научно-технический прогресс" (Новосибиск,1999),
• международной конференции "Мальцевские чтения" (Новосибирск, 2000),
• логическом коллоквиуме LC03 (Хельсинки, 2003).
Результаты диссертации опубликованы в семи работах автора [32] [38].
Остановимся более подробно на содержании работы.
В главе 1 исследуются полимодальные логики на основе а- пространств Ершова.
В параграфе 1.1 приводятся необходимые определения и формулировки известных теорем.
В параграфе 1.2 вводится понятие окрестностной а-шкалы, связанное с понятием а-пространства. При этом рассматриваются пятерки вида (X, Хо, г, , - ), где Хо С X, т — топология на X и , - — бинарные отношения на X.
Для шкал такого вида естественно рассматривать язык полимодальной логики с пятью модальностями: локальной истинностью , определяемой топологией т, временными модальностями , , связанными с отношением , и временными модальностями ! , П , связанными с отношением - . Так как имеется выделенное подмножество, то в язык вводится дополнительная константа /?, которая описывает это подмножество.
В языке с модальностями , , , П , СЦ и дополнительной константой /? формулируется исчисление La. Доказана теорема о корректности LD относительно окрестностных а-шкал.
Кроме того устанавливается связь фрагментов логики LD с известной логикой S4 [15]. В частности, модальные фрагменты с одной модальностью , или совпадают с S4.
В параграфе 1.3 доказано, что топологическая модальность может быть выражена через временные связки. Поэтому естественно рассматривать как сокращение. Исчисление, полученное таким образом из LD, обозначается через La.
Вводится еще одно исчисление L/ языка временной логики с дополнительной константой /?, которое, как оказывается, является синтаксически эквивалентным исчислению La.
Для доказательства финитной аппроксимируемости LD в параграфе 1.4 введены вспомогательные Т-шкалы (с дополнительным отношением Т). Здесь следует заметить, что конечными a-шкалами эти логики нельзя аппроксимировать,так как в конечных a-пространствах, как следует из [1], отношения и - совпадают.
Финитная аппроксимируемость исчисления LD доказывается методом фильтраций (впервые предложенным Леммоном [20], Сегербергом [26], [27]). При этом строится фильтрация канонической модели для LD через некоторое конечное множество Ф и доказывается, что построенная фильтрация основана на Т-шкале. Следовательно, по теореме о полноте исчисления LD относительно Т-шкал (теорема 1.4.2), построенная фильтрация является моделью для LD. Разрешимость I/ следует из разрешимости LD, ввиду предложений 1.3.4, 1.3.5
В главах 2 и 3 исследуются модальная и временные логики, связанные с линейно упорядоченными /-пространствами Ершова. Известна следующая теорема [2]:
Теорема Тройка {X, Хо, } определяется /- пространством тогда и только тогда, когда выполнены условия:
1) Хо С Х отношение является частичным порядком на X;
2) если хо,х 0 Є Хо и существует х Є X такой, что XQ х и х0 х, то в Хо имеется элемент х о = хо U х 0;
3) для любого элемента х Є X существует элемент XQ Є Хо такой, что хо X]
4) для любых элементов х, у Є X, если х у, то существует элемент хо Є XQ такой, что XQ х и хо у.
В параграфе 2.1 вводятся понятия строго линейно упорядоченной /-шкалы и строго линейно упорядоченной /о-шкалы. Тройка (X, Хо, R) называется строго линейно упорядоченной /-шкалой, если выполнены условия:
1) о С X;
2) R является строгим линейным порядком;
3) xRy = Эа?о Є XQ( XRXQ И ( xoRy или хо = у ) ); для любого х Є X существует о Є XQ такой, что xoRx или хо = х. Шкала (X, Хо, R) является строго линейно упорядоченной /о шкалой , если выполнены условия 1)-3) и условие 4о) существует XQ Є Хо такой, что для любых х Є Хверно XQRX ИЛИ XQ = х.
Для шкал такого вида в главе 2 рассматривается язык модальной логики с одним модальным оператором #, и в главе 3 — язык временной логики, с двумя модальностями Пд и n R. Заметим, что модальности , Пч П выразимы через Пд И ПД на рассматриваемых шкалах.
Подчеркнем, что в языке модальной логики с одной модальностью Пд строго линейно упорядоченные /-шкалы и строго линейно упорядоченные /о-шкалы не различаются (теорема 2.3.1). Однако в языке временной логики эти классы шкал различимы (предложение 3.1.1).
В параграфе 2.1 формулируется исчисление Lf.
Кроме того, в параграфе 2.1 вводится понятие F-шкалы. Главным результатом в главе 2 является теорема о полноте исчисления Lf относительно строго линейно упорядоченных /-шкал и строго линейно упорядоченных /о-шкал:
Теорема 2.3.1 Для любой формулы А следующие условия эквивалентны:
1) формула А выводима в исчислении Lf;
2) А истинна во всех строго линейно упорядоченных /о - моделях;
3) А истинна во всех строго линейно упорядоченных / - моделях.
Корректность исчисления Lf доказывается в параграфе 2.1. Для доказательства полноты требуются вспомогательное понятие F-шкал и дополнительное построение. Известно [10], что если формула невыводи-ма в исчислении, то она опровергается в некотором мире канонической модели этого исчисления. Следовательно она опровергается в порожденной этим миром подмодели канонической модели. Но каноническая модель для Lf не является строго линейно упорядоченной /-моделью, хотя и удовлетворяет некоторым свойствам таких моделей. Главная трудность в том, что в канонической модели отношение R, вообще говоря, не обязано быть строгим линейным порядком. Заметим, что для получения строго линейно упорядоченной /-модели в работе используется метод, аналогичный технике "раскатывания" ("bulldozing") [26]. Но задача усложняется тем, что необходимо заботиться о выполнении условий 3), 4), 40).
Так, при построении контрмодели, сначала в параграфе 2.3 специальным образом выбирается счетная подмодель порожденной подмодели канонической модели для Lf. Затем уже строится контрмодель для невыводимой в Lf формулы, являющаяся строго линейно упорядоченной /-моделью.
В параграфе 2.4 доказывается финитная аппроксимируемость Lf конечными F-шкалами.
В главе 3 со строго линейно упорядоченными /-шкалами мы связываем временную логику. В параграфе 3.1 вводятся исчисления L f и L fo, и доказывается корректность L f относительно строго линейно упорядоченных /-шкал и корректность L fo относительно строго линейно упорядоченных /о-шкал.
В параграфе 3.3 доказывается главный результат главы:
Теорема 3.3.1
(1) Формула А выводима в исчислении L f тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /-моделях.
(2) Формула А выводима в исчислении L fo тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /о-моделях.
Для доказательства полноты используется техника, аналогичная технике доказательства полноты Lf в главе 2. Но построения более громоздкие, так как язык содержит, кроме Пд, еще модальность прошлого п В параграфе 3.4 методом фильтраций доказывается финитная аппроксимируемость и, следовательно, разрешимость логик L f и L fo. Здесь необходимо заметить, что аппроксимировать эти логики конечными строго линейно упорядоченными /-шкалами невозможно.
Автор выражает огромную и искреннюю благодарность своему научному руководителю Ларисе Львовне Максимовой за постановку задачи, помощь в работе и неизменное внимание, без которых данная работа вряд ли могла бы быть выполнена.
Модальные логики и шкалы Крипке
Язык n-модальной логики высказываний содержит: а) пропозициональные переменные р\, р2,...; б) логические связки &, V, -і, — ; в) модальные операторы П1?.. .,ПП. Й1/ Модальные связки Oj используются как сокращения, то есть ОІЛ = -іП,—ІІ4. Формулы модальной логики определяются как обычно [10]: пропозициональные переменные являются формулами; если Л и В — формулы, то -іЛ, AVВ, А&В, А — В тоже формулы; если А является формулой, то Пг-Л — формула. Определение 1.1.7 (см., например, [7], [10] ) Шкалой Крипке называется (п + 1)-ка (X, Ri,..., Rn), где X — непустое множество, Ri — бинарные отношения на X. Для n-модальных логик будем рассматривать модели Крипке, и будем говорить об истинности в данный момент времени, где моменты времени - суть элементы множества X. Таким образом, рассмотрим модель вида где (X, R,..., Rn) - шкала , \= - бинарное отношение истинности между X и множеством формул. Отношение = определяется по индукции. Считаем, что для каждой пропозициональной переменной щ и любого х Є X задано одно из двух: х \= pi или неверно, что X \= Pi. Далее по индукции имеем : Если мы рассматриваем временную логику, то с любым бинарным отношением связываем две модальности: D; и D-. Тогда по определению имеем: 6) аф ЩА \/у (yRiX = у\=А). Определение 1.1.8 [10] Говорим, что формула А истинна в модели М, если в каждом мире из М истинна А. Это означает, что для каждого х Є X верно х \= А. В таком случае говорят, что М является моделью для А. Формула А общезначима в шкале F (будем обозначать F \= А), если она истинна в любой модели, основанной на этой шкале. Говорим, что формула А общезначима, если она общезначима во всех шкалах. Приведем некоторые известные логические исчисления (в языке с одним модальным оператором ): Минимальное модальное исчисление К[10]: Аксиомы исчисления К: 1) Все тавтологии; 2) П(Л — B)kUA — ПВ. Правила исчисления К: Ґ) - Минимальное временное исчисление Kt определяется следующим образом [9]: Аксиомы исчисления Kt: Пусть L — любое исчисление, содержащее все аксиомы и правила минимального модального исчисления К (или временное исчисление, содержащее все аксиомы и правила минимального временного исчисления Как обычно, выводом в L называем конечную последовательность формул Лі,..., Ak языка исчисления L такую, что для любого і выполнено: АІ - либо аксиома L, либо есть непосредственное следствие предыдущих формул по одному из правил вывода L. Будем обозначать L Ь А, если формула А выводима в исчислении L. Заметим, что мы будем рассматривать исчисления как с одной, так и с несколькими модальностями. Определение 1.1.9(9] Исчисление L называется полным относительно класса шкал С, если для любой формулы А выполняется: U-A = VFeC(F\=A). 1.1.3 Канонические модели Пусть L — любое модальное или временное исчисление. Обозначим через Ф множество всех формул в исчислении L. Пусть Г —YL А, где А Є Ф, Г С Ф, обозначает, что существуют к 0 и формулы Лі,..., Ак Є Г такие, что (Лі —у ... (Л — А))...) — выводима в L. Определение 1.1.10 Говорим, что множество формул Г является L-противоречивым тогда и только тогда, когда существует В Є Ф такая, что Г — L В и Г — L " -В; L-непротиворечиво в противном случае. Множество Г называется полным, если для любой А Є Ф верно Л Є Г или - А Є Г. Множество Г называется L-теорией, если оно замкнуто относительно — ь. Лемма 1.1.11(6], [26] Любое L-непротиворечивое множество Г-можно расширить до полной L-непротиворечивой L-теории! Пусть Хь - множество полных L-непротиворечивых L-теорий.
Определим отношение R{ (і = 1,..., п) на Хь следующим образом Таким образом возникает шкала (Xi, RI, ..., Rn). Определение 1.1.12 [8], [10] Рассмотрим модель ML — (XL, R\, ..., Rn, \=L) где полагаем x \=L p =$ p x для любой переменной p и любого элемента х Є XL- Назовем Mi канонической моделью исчисления L. Лемма 1.1.13 [9], [15] Если L — временное исчисление, то в канонической модели ML выполнено Лемма 1.1.14(о канонической модели)[15], [10] Для любой А Є Ф, для любого элемента х Є XL верно Доказательство. Утверждение доказывается индукцией по длине формулы . При этом в случае временных исчислений используется предыдущая лемма. Следствие 1.1.15[9], [10] Формула выводима в исчислении L тогда и только тогда, когда она истинна в канонической модели ML Лемма 1.1.16 [15], [28] Пусть L — временное исчисление, тогда в канонической модели ML выполнено (a) если ОІА Є хі, то существует х2 Є XL такой, что А Є х2 и x\RiX2; (b) если О]А б xi, то существует х2 Є XL такой, что А Є х2 и x2Rixi. Определение 1.1.17[9] Говорим, что логическое исчисление L обладает финитно модельным свойством (финитно аппроксимируемо), если для любой невыводимой в L формулы А существует конечная модель для L, в которой А опровергается. Известно, что если L — конечно аксиоматизируемо и обладает финитно модельным свойством, то L является разрешимым [7]. Метод фильтраций является наиболее распространенным методом для доказательства финитной аппроксимируемости модальных логик. Определение 1.1.18 [10], [26], [14] Пусть М = (X, Ru ..., Rn, (=) — некоторая модель и Ф — конечное множество формул, замкнутое относительно взятия подформул. Определим на X отношение эквивалентности =Ф: X=$J/ - = VB Ф(# \= В 4= у \= В). Обозначим через [х] класс эквивалентности, содержащий х, то есть [х] = {у \ у Є X, х =ф у}. Пусть Xі = {[х] х Є X}, тогда М = (X , R lt..., R n, f= ) называется фильтрацией М через Ф, если выполняются условия: (1) xRiy = [хЩуУ, (2) [хЩ[у] = ЧВ{ПНіВ Є Ф и z = П В = у\=В), где г = 1,..., п; (3) [х] \= р == х \= р для любой пропозициональной переменной р. Лемма 1.1.19 (о фильтрации) Если М является фильтрацией М через Ф, то для любой формулы В Є Ф и любого х Є X верно Доказательство Утверждение доказывается индукцией по длине формулы В [9] . Заметим, что в параграфах 1.5, 2.4 и 3.4 фильтрации определяются несколько по-другому. Поэтому мы будем каждый раз доказывать лемму о фильтрации специально. Окрестностной шкалой будем называть пятерку (X, Хо, т, , - ), где Хо Я X, , - — бинарные отношения на X, т — некоторая топология на X. Если {X, XQ, Г, , - ), является а-пространством с базисным подмножеством Хо, то окрестностную шкалу (X, Хо, т, , ) будем называть а-шкалой. Если {X, Хо, т, , - ), является /-пространством и Хо = F(X), то окрестностную шкалу (X, XQ, Т, , - ) будем называть /-шкалой.
Канонические модели для LD и I
По аксиоме (П)4 выполнено Lab О Л —У О (/?& Л), следовательно по аксиоме (I) 1 в La выводима формула О ,, Л —У 0 (/38zO A). (2) Очевидно, что в L выводима формула 0 (/?&П Л) —У 0 .,П Л, следовательно по аксиоме (I) 3 выполнено L h 0 _,(/?& Л) —У О П Л. Таким образом L h 0 (/?&П Л) — Л, то есть в L выводима аксиома (II) 1 исчисления La. Докажем, что L h ПА —У ППА, где О А является сокращением для 0! (/?&;П Л). По аксиоме (II ) 1 в L выводима формула 0! (/3&:П Л) —У О /З&О /З&П Л)). Следовательно в исчислении L выводима формула 0%(РкП А) —У О ЦЗкП О О ркП А)). Тогда по аксиоме (I) 5 верно, что в L выводима формула 0%ЦЗкП А) —У О /З&П О /З&П Л)), то есть в L выводима аксиома (II) 2 исчисления La. Докажем, что в L выводима аксиома (II) 3 исчисления La. Очевидно, что L h 0 ( &П Л) —У П 0 0 (ркП А). Следовательно по аксиоме (1)5 в исчислении L выводима формула OZ,(/?& Л) —у 0! (/?&П Л), то есть L h ПА —у П ПЛ. По аксиоме (И ) 2 L h !,Л —У 0 ,(/3& А), следовательно верно, что L h О Л —У О /Ї&П О О Л). Отсюда по аксиоме (I) 2 получаем, что L h О Л —У О /З&П О Л), то есть в L выводима аксиома (Н)4 исчисления La. По аксиоме (II ) 1 в L выводима 0! (/3&Л) —У О /З&О /З&Л)), следовательно в L выводима формула 0 (/3&Л) —у О /З&О /З&Л)), то есть акиома (II) 5 исчисления La. Предложение 1.3.3 доказано. Предложение 1.3.4 Для любой формулы Л верно: А выводима в La тогда и только тогда, когда Л выводима в L . Доказательство Утверждение сразу следует из предложения 1.3.3. Докажем еще одно предложение о связи исчислений La и LD, которое нам понадобится в параграфе 1.5. Каждой формуле Л языка исчисления LD сопоставим некоторую формулу языка исчисления La следующим образом: заменяем все подфор мулы формулы А вида ПВ на формулы О Р&П В). Результат такой замены (в формуле А) обозначим через Аа.
Предложение 1.3.5 Для любой формулы А верно: Аа выводима в La тогда и только тогда, когда А выводима в LD. Доказательство Пусть формула Аа построена по формуле А и Аа выводима в La. Тогда существуют формулы А\,..., Ak = Аа языка исчисления La такие, что для любого і выполнено: АІ — либо аксиома La, либо есть непосредственное следствие предыдущих формул по одному из правил вывода La. Если АІ — аксиома La, то она получена из некоторой аксиомы Д-исчисления LD, то есть А( = Віа. Тогда по предложению 1.3.1 (2) В\,..., В/- является выводом формулы Аа в исчислении LD. По предложению 1.3.1 (1) тогда LDh А. Пусть формула Аа построена по формуле А и А выводима в LD. Тогда существуют формулы А\,..., Ak = А языка исчисления LD такие, что для любого і выполнено: Аі — либо аксиома LD, либо есть непосредственное следствие предыдущих формул по одному из правил вывода LD. Тогда Аа\,..., Aak выводимы в исчислении La по предложению 1.3.1, следовательно Lab Аа. 1.4 Канонические модели для La и L/ Пусть X — множество полных La-HenpoTHBope4HBbix LDeopnu, XQ = {х Є X /З Є х}. Определим отношения R на X следующим образом где R Є { , }. Введем дополнительное отношение Т на множестве X, связанное с модальным оператором : Таким образом возникает шкала (XL, XQ, , - , Т). Рассмотрим каноническую модель МІР = (X, XQ, , - , Т, =і) для LD, где х \=L р = р Є х, х [=, /3 = /З Є х для любой переменной р и любого элемента х Є X. Свойство (МI) 5 доказывается аналогично. Докажем свойство (МII) 3. Пусть х yTz и ПА Є х. Тогда по аксиоме (II) 3 выполнено П ПА Є х, следовательно ПА Є у, следовательно А Є z. Таким образом хТу и пункт (МII) 3 доказан. # Докажем свойство (МП)4. Пусть х - yTz. Предположим, что не верно, что х z. Тогда существует формула В такая, что Є z и В 6 х, следовательно 0 - В Є у так как х - у. Так как yTz, то OD B Є г/. Тогда по аксиоме (II) 4 выполнено П В Є г/, что противоречит тому, что О -іВ є у. Следовательно х z. Докажем свойство (МII) 5. Пусть х X и 5 = {А \ П А Є х} U и{пв ПВ ex}U{(3}. Докажем, что множество s является непротиворечивым. Предположим противное, тогда существуют формулы П Лі,..., П Лд Є х, ?i,..., ПВк Є х, такие, что в LD выводима формула Следовательно LDh П! (Лі&... SzAk) — а -.(Пі&... кПВк&,/3). Так как П АІ Є х, 1 і п, то П -І(ПВІ&...&ПБ)Ь&І9) Є х, то єсть -.0 (0(5 ...&В )&/3) Є х. Так как 0 є ж, 1 j к, то (Ві&...&ДО Є ж. Следовательно, формула что противоречит выводимости в LD формулы (?!& ... к.Вк) — —у 0 (П(Ві&.. .&БА;)&;/3). Таким образом множество s является непротиворечивым. Следовательно по лемме 1.1.11 множество s можно расширить до Ь-непротиворечивой полной Ьп-теории XQ. Очевидно, что XQ Є XQ, так как /З Є XQ. Из определения отношения - в канонической шкале следует, что XQ - х. Докажем, что XTXQ. Пусть ПА 6Е х, тогда ПА Є XQ, следовательно по аксиоме (II) 1 выполнено А Є XQ, ТО есть XTXQ, И теорема 1.4.1 доказана. Введем понятие Т-шкал. Т-шкалой будем называть пятерку (X, XQ, , - , Т) , удовлетворяющую условиям (МІ), (МП). Модель, основанную на Т-шкале будем называть Т-моделью. Таким образом, каноническая модель для LD (X, XQ, , - , Т, \=ьа) является Т-моделью. Теорема 1.4.2 Формула А выводима в исчислении LD тогда и только тогда, когда А истинна во всех Т-моделях. Доказательство Легко показать, что аксиомы исчисления общезначимы в шкалах, удовлетворяющих условиям (Ml), (МП). Достаточность следует из теоремы 1.4.1 и следствия 1.1.15. Рассмотрим теперь каноническую модель Ми = {X, XQ, , - , \=L ) для I/, где X — множество полных L -непротиворечивых L -теорий, отношения , - определены выше, х \=и р -= р G х, х \=L (3 = р Є х для любой переменной р и любого элемента х Є X. Теорема 1.4.3 (о канонической модели для L ) Каноническая модель Ми = {X, Хо, , - , \=и) для I/ удовлетворяет условиям (Ml) теоремы 1.4.1 и следующим условиям: (МII ) 1) XQ, XQ Є ХО И Хо И х 0 - X = BX Q Є XQ{ XQ - X И XQ - , XQ И x0 " xo) 2) X - у = XQ Є XQ( X XQ И XQ - y). Доказательство Пусть XQ, X 0 Є XQ И XQ - x, x Q - x. Положим s = {O A А Є x0} U {0%B В Є x0}\J U{C П С Є x} U {/3}. Докажем, что множество s является непротиворечивым.
Предположим противное, тогда существуют формулы А\,..., А\ Є XQ, В\,..., Вп Є х 0, Ci,...,CkGx такие, что в I/ выводима і/ь о (Аад&...& (А»&:/з) — о;(0! (Аед&...&о! (і педад. Таким образом, по лемме 1.1.11 множество s можно расширить до L -непротиворечивой полной L -теории X Q. Очевидно, что X Q XQ, так как /З Є X Q. ИЗ определения отношений и - в канонической шкале следует, что XQ S XQ, X s XQ, XQ s X . 4 Докажем свойство 2). Пусть х - у, положим s = {А \ П А Є y}U U{0 B \ВЄх}и {/?}. Докажем, что множество s является непротиворечивым. Предположим противное, тогда существуют формулы П Лі,..., U Ai Є у, В\,..., Вп Є x такие, что в I/ выводима Лі&... hAi —- і(О Бі&... 0 Bnkp). Следовательно L h Агк... &AZ —)- -i(0(Bi&... ВП)Щ. Таким образом L h D Aife... &П! Л — -.0:,(0 (5 ... „)&/?)). giK Так как П Д Є j/, то -.0 (0 (5 ... „)&/?)) Є у. Так как Бу Є ж и х - т/, то 0 (5і&...&5„) Є у. Таким образом 0 (Бі&... &Б„)&-.0!{(0 (Бі&;... Вп)кр)) Є /, что противоречит аксиоме (IF) 2. Следовательно, по лемме 1.1.11 5 можно расширить до L -непротиворечивой полной L -теории х 0. Очевидно, что х 0 Хо, так как /З Є ж0- Из определения отношений и - в канонической шкале следует, что х XQ и XQ - у. J Введем понятие сё-шкалы. Четверку (X, XQ, , - ) будем называть 5-шкалой, если она удовлетворяет свойствам (М I), (МII ) теоремы 1.4.3. Модель, основанную на а-шкале назовем а-моделью. Как следует из теоремы 1.4.3, каноническая модель для I/ является а-моделью. Предложение 1.4.4 Если шкала (X, Хо, , - , Т) является Т-шкалой, то шкала (X, Хо, , - ) является й-шкалой. Доказательство п Свойства (Ml) очевидно выполняются для {X, Хо, , - ). Пусть хо, х о Є А о и XQ - х и х 0 - х. По пункту (МII) 5 существует х 0 Є Хо такой, что х 0 - х и жТжд. Следовательно по пункту (МII) 5 существует wo Є Хо такой, что WQ - х о и X QTWQ. ПО транзитивности отношения Т тогда XTWQ. Так как хо - ж и XTWQ, то жо и о по свойству (МИ)4. Аналогично x Q WQ. Таким образом хо wo X Q и х 0 WQ - ж0 . Следовательно по свойству (М I) 5 XQ - X Q И X Q - a?g и свойство (М И ) 1 доказано. Пусть а; - у. По пункту (МП)5 теоремы 1.4.1 существует XQ Є XQ ч такой, что хо - у и уТхо. Так как ж - уТхо, то по свойству (МII) 4 выполнено ее XQ, и предложение 1.4.4 доказано. Теорема 1.4.5 Формула А выводима в исчислении I/ тогда и только тогда, когда А истинна во всех й-моделях. Доказательство Необходимость следует из того, что аксиомы исчисления общезначимы в шкалах, удовлетворяющих условиям (Ml), (МІГ). Достаточность следует из теоремы 1.4.3 и следствия 1.1.15.
Lf и структура канонической модели
В этом параграфе мы установим некоторые свойства канонической модели для Lf, и докажем теорему о полноте исчисления Lf относительно F- моделей. Лемма 2.2.1 В Lf выводимы формулы ОЛі&... &ОАп — 0(/?&(ОІ4І V Лх)&... &(ОЛ„ V Ап)) для любого п 2 . Доказательство. Докажем утверждение леммы индукцией по п. Базис индукции для п — 2 очевиден. Пусть выводима ОЛі&... кОАп — 0(/?&(ОІ4І V І4І)& ... к(ОАп V Ап)) для некоторого п 2. Тогда выводима OAi&...&OAn&OAn+l — 0( &(ОЛіУЛі)&...&:(ОАпУАп))&ОЛп+і . Следовательно, выводима % ОЛі&... &ОЛ„&ОЛп+і —у 0(/?&(0(&(ОЛі V Лі)&... &(ОЛп V Лп)) V /3&(ОАі V Лі)&... к(ОАп V Л„))&(ОАп+1 V А,+і)) , т. е. выводима ОЛі&... &ОАпкОАп+1 —+ 0(/?&0(ОЛіУАі)&... &0(OAnVAn)k(OAn+ Ап+І)) . Таким образом выводима следующая формула ОЛі&... &ОЛп&ОЛп+і —у 0{Рк(ООАі V ОАх V Ах)к... &(ООЛп V ОАп\/АпЩОАп+1\ґАп+1)) . Ш Так как Lfh ООЛ — О А , то выводима OAik... &ОАп+1 —У 0(/3&(0;4і Vi4i)&... &(OAn+i VAn+i)) , что и требовалось. Рассмотрим каноническую модель ML/ = {XLJ, / RLJ, И) Для Lf, где полагаем Xif — множество полных Lf-непротиворечивых Lf-теорий, XLf = {xXLf\pe х}, W x \= p = p Є x для любой переменной р и любого элемента х Є Хх,. Пусть L — модальное исчисление, содержащее К, ML = {XL, X, RL, \=) каноническая модель для L. Предложение 2.2.2 Если в исчислении L выводима формула ОЛі&... &ОД, — 0(рк(ОАі V Лі)&... &{ОАп V Ап)) , то для любых х, у Є XL выполнено Доказательство. Положим х 0 = {А DA Є х} U {ОБ V Б Б Є у} U {/?} . Докажем, что множество х 0 является непротиворечивым. Предположим противное, тогда существуют формулы ПА\,..., О А}- Є х , J5i,..., Вп Є у , такие, что выводима Следовательно, выводима как (З Є XQ. ИЗ определения отношения RL В канонической шкале следует, что XRLXQ И ( XQRLV или хо = у ) . Теорема 2.2.3 (о канонической модели для Lf) Каноническая модель для Lf удовлетворяет условиям : 1) RL/ является транзитивным отношением ; 2) xRLfy = Зхо Є Xlf( XRLJXQ и ( x0RLfy или х0 = у ) ) ; 3) если tRbfX, tRb/y, х фу, то XRL/У ИЛИ yRijx. Доказательство. Свойства 1), 3) доказаны ранее в [9]. Свойство 2) следует из предложения 2.2.2 и леммы 2.2.1. Пусть Мщ = (Х у, XQ, R f, \=l) - порожденная некоторым элементом t Є XL/ подмодель канонической модели, то есть Х ь = {х \ х Є XLf, tRLfx или t = х}, Х 0 = XLf П Xі, Rif = RLf\x Lf, 1=-(= \х ь, Верны следующие утверждения: Лемма 2.2.4 (о порожденной подмодели) Пусть М1 = (Xі, R , (= ) порожденная некоторым элементом t Є X подмодель модели М = {X, R, \=). Тогда для любой формулы А и любого х Є Xі верно Доказательство. Лемма доказывается индукцией по длине формулы [26]. Предложение 2.2.5 Порожденная подмодель Мь канонической модели для Lf является F-моделью. Доказательство. Утверждение следует из определения порожденной подмодели и теоремы 2.2.3 о канонической модели для Lf. Теорема 2.2.6
Для любой формулы А верно: А выводима в Lf тогда и только тогда, когда А истинна во всех F-моделях. Доказательство. Необходимость следует из теоремы 2.1.1. Пусть А невыводима в Lf, и А истинна во всех F-моделях. Тогда А опровергается в канонической модели для Lf в некотором мире t. Следовательно по лемме 2.2.4 формула опровергается в М1. По предло щ жению 2.2.5 модель Мь является F-моделью. Таким образом получаем противоречие с тем, что А истинна во всех F-моделях, следовательно А выводима в Lf. Цель этого раздела — доказать теорему 2.3.1 о полноте исчисления Lf относительно строго линейно упорядоченных /о - моделей и строго линейно упорядоченных / - моделей. щ Заметим, что из теоремы 2.3.1 вытекает следующее: в языке мо дальной логики (с одним модальным оператором ) строго линейно упорядоченные /-шкалы и строго линейно упорядоченные /о-шкалы не различаются. В главе 3 мы покажем, что в языке временной логики (с двумя модальными операторами , ) строго линейно упорядоченные /-шкалы и строго линейно упорядоченные /о-шкалы различимы (предложение 3.1.1). )& Теорема 2.3.1 Для любой формулы А следующие условия эквива лентны: 1) формула А выводима в исчислении Lf; 2) А истинна во всех строго линейно упорядоченных /о-моделях; 3) А истинна во всех строго линейно упорядоченных /-моделях. Доказательство. То, что из пункта 1) следует пункт 2) сразу вытекает из теоремы 2.1.2 о корректности. Так как строго линейно упорядоченная /о-модель а является строго линейно упорядоченной /-моделью, то из 3) следует 2). Докажем, что из пункта 2) следует пункт 3). Для доказательства необходимы дополнительные построения. Пусть формула А невыводима в Lf, тогда существует элемент t Є Xif такой, что ty=- А . Пусть М = (X, XQ, R, (=) - порожденная элементом t подмодель канонической модели для Lf. Рассмотрим множества подформул Sub(A) формулы А (мы предполагаем, что формула А содержит модальности только вида О А,). Выбираем элементы из X следующим образом: Если t (= ОВІ, где ОВ{ Є Sub(A), то существуют уі Є X такие, что tRyi и уі (= ВІ . Далее на этих элементах уі проверяем истинность всех формул из множества Sub(A). Если уі (= OCj, где OCj Є Sub(A), то существуют z Є X такие, что yiRzij и Z{j \= Cj . Добавляем к t, у І элементы Z{j, и теперь на элементах Zij проверяем истинность всех формул из множества Sub(A), и т. д. Таким образом формируем счетное множество Х = {t, у І, Z\J, ...}, Х С X . На следующем шаге рассмотрим все пары в Х \ Пусть х,у Є Х и xRy . Если не существует элемента XQ Є XQ П X такого, что XRXQ И ( xoRy или XQ = у ), то добавляем к Х некоторый элемент х 0 Є XQ, такой, что XRX Q И ( x 0Ry или х 0 = у ). Такой х 0 найдется по предложению 2.2.5. Таким образом рассматриваем все пары в Х и добавляем, если нужно, элементы из XQ. Полученное множество обозначим через Таким образом, на четном шаге к — 2г проверяем на элементах Х к 1 истинность всех формул из множества Sub(A), и добавляем к Х к 1 нужные элементы, формируя множество Х к\ На нечетном шаге к = 2г + 1 формируем множество Х к\ рассматривая все пары Х(к и добавляя к Х к недостающие элементы из Пусть X = U X, X Q = Xі П ХО, В! = R\x», \= - ограничение отношения \= на Xі. Заметим, что X является счетным множеством, так как на каждом шаге добавляли не более чем счетное множество элементов из X. Щ Лемма 2.3.2 Для любого х Є X и любой формулы В Є Sub(A) верно
Канонические модели для L*f и L*fo
Теорема 3.2.1 (о канонических моделях) (a) Каноническая модель ML / = (X, XQ, R, \=L f) Для L f удовлетво ряет условиям 1) R является транзитивным отношением; 2) если tRx, tRy, х фу, то xRy или yRx, если xRt, yRt, хфу, то xRy или yRx; 3) xRy =$ Зяо XQ( XRXQ и ( xoRy или XQ = у ) ); 4) для любого х Є X существует XQ Є ХО такой, что XQRX ИЛИ XQ = X. (b) Каноническая модель ML /0 = {X, Хо, R, \=ь /0) для L fb удовлетво ряет условиям 1)-3) пункта (а) и условию 4о) для любого х Є X существует о Є XQ такой, что XQRX ИЛИ XQ = х и не существует у Є X такого, что yRxQ. Доказательство. Свойства 1), 2) следуют из аксиом 1), 2) и доказаны ранее в [15]. Свойство 3) следует из предложения 2.2.2 и леммы 2.2.1. Докажем пункт 4) теоремы. Пусть х Є X, тогда по лемме о канонической модели 0 Р V /З Є х, следовательно 0 /3 Є х или /З Є х. Если (З Є х, то х Є XQ ПО определению канонической модели, если 0 /3 Є х, то по лемме 1.1.16 получаем, что существует хо Є X такой, что /З Є XQ и XQRX. Следовательно существует XQ Є Хо такой, что XQRX ИЛИ XQ = х. Докажем пункт 40). Пусть х Є X, тогда 0 (/3&D _L) V (/?& _!_) Є х, следовательно 0 ( &D J_) Є х или /3&П А. Є х. Если /?& !. Є ж,то /З (Е ГЕ, то есть Ї 6 Хо, и ! ж. Докажем, что тогда не сушествует у Є X такого, что yRx. Предположим противное. Так как П і_ Є х и у/йг, то по лемме 1.1.13 і. Є г/. Это противоречит условию, что у является полной I/fb-непротиворечивой I/fo-теорией. Если 0 (j3$zO ±.) є х, то по пункту (Ь) леммы 1.1.16 получаем, что существует XQ Є X такой, что XQRX и /3&;П _1_ Є XQ. Аналогично предыдущему доказательству имеем, что XQ Є Хо и не существует у Є X такого,, что yRxo. Таким образом, для любого х Є X существует яо Є Хо такой, что XQRX ИЛИ ХО = х, и не существует у Є X такого, что yRxQ. Теорема 3.2.2 (1) Формула А выводима в исчислении L f тогда и только тогда, когда А истинна во всех моделях, удовлетворяющих условиям 1)-4) те . оремы 3.2.1. (2) Формула А выводима в исчислении L fb тогда и только тогда, когда А истинна во всех моделях, удовлетворяющих условиям 1)-3), 4о) теоремы 3.2.1 Доказательство.
Необходимость сразу следует из предложения 3.1.1. Достаточность следует из теоремы 3.2.1 и следствия 1.1.15. 3.3 Теорема о полноте относительно строго линейно упорядоченных /-моделей Цель этого раздела — доказать следующую теорему о полноте исчисления L f относительно строго линейно упорядоченных /-моделей и исчисления L fb относительно строго линейно упорядоченных /о-моделей: Теорема 3.3.1 (1) Формула А выводима в исчислении L f тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /-моделях. (2) Формула А выводима в исчислении L fo тогда и только тогда, когда А истинна во всех строго линейно упорядоченных /о-моделях. Доказательство. Необходимость следует из теоремы 3.1.2 о корректности. Для дока зательства достаточности потребуются дополнительные построения. ц Пусть формула А невыводима в L f, тогда существует элемент t Є X канонической модели ML / = (X, Хо, R, \=L f) для L f такой, что t \fcb f A . Выберем специальным образом счетную подмодель канонической модели для L f. Рассмотрим множество подформул Sub(A) формулы А (можем считать, что формула А содержит модальности только вида О и О ). Выбираем элементы из X следующим образом: . Если t \=L f ВІ, где ОД- G Sub(A), то существуют уі X такие, что tRyi и у І \=L f В І . Если t \=L f 0 ВІ, где 0 В{ Є Sub(A), то существуют у і Є X такие, что y\Rt и у\ \=L J ВІ . Далее на этих элементах у І, у[ проверяем истинность всех формул из множества Sub(A). Если уі \=ь / Cj, где OCj Є Sub(A), то существуют z Є X такие, что ytRzij и 2 \=L f Cj . Если у\ \=L f Cj, где 0 Cj Є Sub(A), то существуют z\j Є X такие, что z Ry i и z\j \=L-f Cj . Добавляем Kt, уі, у[ элементы Zij, z\j, и теперь на элементах z , z\j проверяем истинность всех формул из множества Sub(A), и т. д. Таким образом формируем не более чем счетное множество Х = & ф у[, t, уі, Zij,...}, Х СХ. На следующем шаге рассмотрим все пары в Х \ Пусть х,у Є Х и xRy . Если не существует элемента XQ Є Хо П Х такого, что XRXQ и ( xoRy или хо = у ), то добавляем к Х некоторый элемент х 0 Є Хо, такой, что XRX Q и ( x 0Ry или х 0 = у ). Такой х 0 найдется по теореме 3.2.1. Таким образом рассматриваем все пары в Х и добавляем, если нужно, элементы из Хо. Если в полученном множестве есть наименьший элемент я и он не принадлежит Хо, то добавляем некоторый х$ Є Хо такой, что XQRX. Такой XQ найдется по пункту 4) теоремы 3.2.1. Полученное множество обозначим через Л" . Таким образом, на четном шаге к = 2г проверяем на элементах истинность всех формул из множества Sub(A), и добавляем к Х к нужные