Неподвижные точки модальных операторов

Оглавление
Введение 3
1 Позитивные П-операторы 15
1.1 Формульные операторы......................................... 15
1.2 Примеры.......................................................21
1.3 Строго частично упорядоченные модели с обрывом возрастающих цепей.........................................................27
1.4 Частично упорядоченные модели с обрывом возрастающих цепей 48
1.5 Модели с условием конфинальности бесконечных возрастающих цепей ............................................................60
2 Позитивные операторы 83
2.1 Е-операторы...................................................83
2.2 Модели с обрывом возрастающих цепей...........................89
2.3 Модели с условием слабой конфинальности бесконечных возрастающих цепей....................................................111
2.4 Определимость без сохранения позитивности ...................138
2.5 Предупорядоченные модели.....................................170
2.6 Негативные операторы.........................................178
3 Временные операторы 189
3.1 Позитивные П-операторы.......................................189
Литература 226
Предметный указатель 232
2
Введение
При любом преобразовании объектов какой-то объект может остаться неизменным. Тогда это — неподвижная точка. Так же как идея отображений, преобразований пронизывает математику, так и неподвижные точки широко встречаются во всей математике. Неподвижные точки прямо имеются в виду, когда отображение или процедура описывается реку1>сивно. Определение также может быть индуктивным, в этом случае определяемое множество объектов является неподвижной точкой.
Начало исследований неподвижных точек в областях, близких к данной работе, можно отнести к 20-м годам 20-го века. Б.Кнастер и А.Тарский рассматривали неподвижные точки операторов, действующих на подмножествах некоторого множества 49). Неподвижные точки отображений решеток исследовались А.Тарским [74, 75].
Операторы могут содержать параметры. Неподвижная точка называется определимой, если она выражается через эти параметры. При этом естественно соблюдать баланс с{>едств. т.е. пользоваться теми же средствами, что и при составлении оператора. В исследовании неподвижных точек можно выделить два случая: неподвижные точки определимы и не определимы. В случае, когда неподвижные точки не определимы, добавление оператора неподвижной точки увеличивает выразительную силу. Если неподвижные точки определимы, то это означает, что в системе достаточно средств для их выразимости. Данная работа посвящена определимым неподвижным точкам.
В теории модальных логик имеется широко известная теорема о неподвижной точке, значение которой выходит за рамки неклассических логик. Эта теорема утверждает определимость и единственность неподвижной точки мо-дализованного оператора в модальной логике Геделя-Леба, связанной с арифметической доказуемостью. Историю доказательства теоремы можно найти в (59, 69, 71, 72). Сначала К. Бернарди (25, 26] и К. Сморинский (анонсировано в [68]) доказали ее в частном случае. В полном виде теорему доказали Д. де Йонг (не опубликовано) и Дж. Самбин [62]. Другие доказательства этой
3
ВВЕДЕНИЕ
4
теоремы можно найти в (28, 30, 46, 59, 63, 69, 72] (см. также комментарии в [56, 57]), она упоминается в [70]. Имеются ее бимодальные и полимодальиыс варианты [72, 48], а также аналоги в логике интерпретируемости [36].
Интересную теорему о неподвижной точке для интуиционистской пропозициональной логики доказал В. Руитенбург [60].
Другим важным примером является теорема Р. Ганди [42] в теории допустимых множеств, см. также [24, 2]. Она утверждает Е-определимость наименьших неподвижных точек Е-операторов и находит применение в логическом программировании [1].
Имеются разные варианты определимости. Бывает, что определяющая формула не зависит от модели данного класса, можно назвать такую определимость равномерной. Когда говорят об определимости, обычно имеют в виду этот случай. Иногда определяющая формула зависит от модели. При этом возможно, что определяющих формул набирается бесконечное число, но может произойти интересный случай, когда достаточно конечного числа формул. Такой эффект в данной работе исследуется.
Бели неподвижные точки не определимы, то язык можно обогатить оператором неподвижной точки - наименьшей, наибольшей и других. Таким способом, например, получаются /> исчисления. Смысл такого обогащения состоит в том, чтобы увеличить выразительную силу в нужном направлении и при этом получить логику с хорошими свойствами. В [65] впервые описана введенная Д.Скоттом математическая теория рекурсивных процедур. Она основана на той идее, что рекусивные процедуры - это наименьшие неподвижные точки преобразований (об этом написано также в [35]). Пропозициональная версия - модальное ^-исчисление - было введено Д.Козеном в [50]. Оно является фрагментом монадической логики второго порядка и обладает многими хорошими и интересными свойствами [51, 34). Например, //-исчисление обладает униформной интерполяцией. Интересно отметить, что логика первого порядка не обладает униформной интерполяцией. О неподвижных точках и логике, получаемой добавлением оператора наименьшей неподвижной точки к логике первого порядка, можно прочитать в книгах [58, 23, 38].
Вообще говоря, позитивность не всегда совпадает с монотонностью. Даже в этом случае позитивные операторы составляют важнейший подкласс монотонных. Они задаются простым, легко проверяемым синтаксическим условием позитивности. Одним из затруднений, связанным с монотонностью, является то, что монотонность может не устанавливаться алгоритмически.
Еще одна область исследований непосредственно примыкает к неподвижным
ВВЕДЕНИЕ
5
точкам — это решение уравнений, так как неподвижная точка является решением уравнения особого вида. В свою очередь разрешимость уравнений тесно связана с допустимостью правил вывода. В [40] X.Фридманом поставлена проблема №40: разрешима ли алгоритмически проблема допустимости правил вывода в интуиционистской пропозициональной логике? А.В.Кузнецовым была поставлена проблема: обладает ли эта логика конечным базисом для допустимых правил? Основные результаты в этой области получены В.В.Рыбаковым. В [20] проблема X.Фридмана решена положительно. Найден критерий допустимости правил вывода в модальной системе 54 и интуиционистской пропозициональной логике. Из критерия вытекает алгоритмическая разрешимость проблемы допустимости правил вывода в 54 и интуиционистской пропозициональной логике. В [21] проблема А.В.Кузнецова решена отрицательно. Основы используемой техники заложены в [19]. В [22] доказано существование алгоритма, распознающего разрешимость уравнений в свободной топобулевой алгебре и свободной псевдобулевой алгебре, эффективно строится решение разрешимых уравнений. Теория допустимых правил изложена в книге [61]. С.Гиларди доказал конечность числа наиболее общих решений в интуиционистской логике [45] и некоторых модальных логиках [43, 44].
Исследование определимости неподвижных точек находится в русле работ по определимости неявно определенных объектов. Сюда относятся интерполяционная теорема В.Крейга [32], интерполяционная теорема Р.Линдона [52] (по поводу этой статьи см. также [73, 47]), теорема Е.Бета об определимости [27 , проективное свойство Е.Бета [37] и др. Что касается модальных логик, то в [41, 33, 64] была доказана интерполяционная теорема для некоторых модальных логик, для некоторых анонсирована (см. также комментарий к последней статье в [5]). Л.Л.Максимовой в [3] даны алгебраические эквиваленты разных форм интерполяционного свойства и доказана конечность числа модальных логик. расширяющих 54 и обладающих интерполяционным свойством, а в [5] доказана интерполяционная теорема для многих модальных логик. Дж.Булосом [29] доказана интерполяционная теорема для логики Сгг Л.Л.Максимовой найдены алгебраические эквиваленты свойств Бета [9], проективных свойств Бета [10] и указаны взаимосвязи между различными вариантами свойства Бета и интерполяционного свойства. Доказательство аналогов теоремы Линдона для нескольких модальных логик можно найти в [39, б].
До сих пор в модальной логике исследовались модализованные операторы и их неподвижные точки. Это объясняется связью таких операторов с фор-мальной арифметикой. Развитие теории монотонных и позитивных операто-
ВВЕДЕНИЕ
6
рои в других областях логики потребовало создания аналогичной теории в модальной логике. Как мы видим, это направление находится в тесной связи со многими направлениями математической логики. Все они сейчас активно развиваются.
Целью работы является создание теории определимости неподвижных точек модальных операторов: получение широких достаточных условий определимо-сти наименьших неподвижных точек позитивных операторов, их подклассов, определимости одной формулой, конечным числом формул, определимости с сохранением позитивности параметров и без сохранения; достаточных условий единственности и определимости неподвижных точек негативных операторов.
Основные результаты диссертации.
1) Доказана определимость наименьших неподвижных точек позитивных операторов в IКЕ-моделях. Класс ШЕ-моделей введен в данной работе и охватывает большую часть моделей, в которых наименьшие неподвижные точки позитивных операторов определимы. Построены контрпримеры к определимости. Они основаны на моделях, находящихся очень близко к /Я-Е-моделям.
2) Доказана определимость с сохранением позитивности параметров наименьших неподвижных точек позитивных операторов в частично упорядоченных и строго частично упорядоченных моделях с условием слабой конфинальности бесконечных возрастающих цепей. Эти классы моделей также введены в данной работе и охватывают большую часть моделей, в которых наименьшие неподвижные точки позитивных операторов определимы с сохранением позитивности.
3) Исследованы подклассы позитизных операторов: позитивные ^-операторы и П-операторы. Для позитивных Е-операторов доказана определимость наименьших неподвижных точек в транзитивных моделях. Для позитивных П-операторов доказана определимость конечным числом формул наименьших неподвижных точек в частично упорядоченных и строго частично упорядоченных моделях с условием конфинальности бесконечных возрастающих цепей. Обнаруженная здесь определимость конечным числом формул является весьма интересным вариантом определимости.
4) Доказано, что наименьшие неподвижные точки позитивных операторов определимы в предупорядоченных моделях с ограниченным числом перемен истинности.
5) Для негативных операторов доказана единственность неподвижных точек в моделях с сильным условием обрыва возрастающих цепей и определимость в транзитивных моделях с сильным условием обрыва возрастающих цепей.
ВВЕДЕНИЕ
7
G) Доказана определимость наименьших неподвижных точек временных позитивных П-операторов в конечных линейно упорядоченных и строго линейно упорядоченных моделях, а также в бесконечных моделях: основанных на натуральных и целых числах с естественным линейным и строгим линейным порядком.
В диссертации исследуются операторы, которые можно задать формулой в моделях Крипке. Пусть дана формула <p(p,qi,.. .,qn)- Рассмотрим модель Кринке ( W, R, v), в которой заданы значения Qu..., Qn переменных qit... ,qn, а значение переменной р не задано. Формула <р(Р>4ь • • • ><?«) определяет на модели Крипке (W,R,v) оператор FV(P) = <р(Р, Qu..., Q„), который каждому множеству Р сопоставляет множество <р(Р, ..., Qn). Т.е. переменной р при-
дается значение; Р и рассматривается значение формулы <р при этом означивании. Такие операторы назовем формульными. Переменные qi,...,qn будем называть параметрами этого формульного оператора F^. Если каждое вхождение переменной р в формулу <p(p>qi,... ,<уп) позитивное, то назовем эту формулу позитивной по р, а оператор Fv назовем позитивным. Если каждое вхождение переменной р в формулу <р(р, q\,... ,qn) модализованное, то назовем эту формулу модализованной по переменной р, а оператор F,fi назовем мобилизованным. Модальной 11-формулой называем формулу, составленную с помощью связок А, V, □ из формул, не содержащих ни □, ни 0. Если формула <р(р, Ц\,..., qn) является П-формулой, то оператор F# называем П-оператором. Множество Р называется неподвижной точкой оператора FP, если выполняется Р = Р9(Р).
Если неподвижная точка Р совпадает в модели со значением некоторой формулы иф/1,..., </„), то эта формула to определяет неподвижную точку Р в данной модели. Называем эту формулу определяющей. Определяющая формула • • •, Яп) сохраняет позитивность параметров, если для любого параметра уг выполняется следующее: если формула <р(р, , qn) не содержит негатив-
ных вхождений параметра ql: то и <}юрмула u>(q\,... ,qn) не содержит негативных вхождений qi. Будем использовать обозначения (За- = а А Па, Qor = aVOa.
В первой главе исследуются позитивные 11-операторы. Во втором параграфе приведены несколько важных примеров наименьших неподвижных точек, не я в л я ющи хся определим ы м и.
В третьем параграфе рассмотрены строго частично упорядоченные модели Крипке с обрывом возрастающих цепей. Имеется известная теорема о неподвижной точке, принадлежащая К. Бернарди, Д. де Йонгу, К. Сморинскому и Дж. Самбину. Эквивалентная формулировка в терминах моделей такова
ВВЕДЕНИЕ
8
Теорема о неподвижной точке. Для любого модал изованн ого оператора его неподвижная точка в любой строго частично упорядоченной модели Крипке с обрывом возрастающих цепей существует и единственна и, кроме того, существует формула о?, определяющая эту точку во всех таких моделях.
Доказано предложение о сведении позитивного случая к модализованному. С помощью этого предложения из теоремы о неподвижной точке получаем теорему 1.3.6, утверждающую, что в рассматриваемых моделях наименьшая неподвижная точка позитивного П-оператора определяется некоторой П-формулой, единой для всех таких моделей. При этом определяющая формула сохраняет позитивность параметров.
Далее будут рассматриваться более сложно устроенные модели, на которые упомянутая теорема о неподвижной точке не распространяется. Поэтому разработана конструкция опровергающих конфигураций, которая в дальнейшем будет использоваться для более широких классов моделей. Она также дает алгоритм построения определяющих формул. С ее помощью в этом параграфе дано другое доказательство теоремы 1.3.6. Из этой теоремы получаем следствие 1.3.27 для модальной логики Геделя-Леба СЬ. Далее рассмотрены операторы с несколькими аргументами. Для таких позитивных П-оиераторов доказана аналогичная тео}юма об определимости наименьших неподвижных точек. Важность сохранения позитивности параметров состоит в том, что оно позволяет использовать метод исключения неизвестных.
В четвертом параграфе рассмотрены частично упорядоченные модели Крипке с обрывом возрастающих цепей. На них теорема о неподвижной точке не распространяется, поэтому доказательство теоремы 1.4.1 об определимости наименьших неподвижных точек позитивных 11-операторов дано с помощью опровергающих конфигураций, несколько модифицированных для данного случая. Алгоритмы построения определяющей П-формулы для строго частично упорядоченных и частично упорядоченных моделей различны. Это различие существенно, в конце параграфа приведен пример 1.4.21, показывающий, что единую для этих случаев П-формулу построить, вообще говоря, нельзя.
В пятом параграфе расширяется класс моделей, в которых определимы наименьшие неподвижные точки позитивных П-оиераторов. Однако, определимость здесь несколько другая. Если в моделях с обрывом возрастающих цепей было достаточно одной П-формулы, то здесь нужно коночное число 11-формул. Вводится понятие шкалы с условием конфинальности бесконечных возрастающих цепей. Сначала рассмотрены частично упорядоченные шкалы с условием конфинальности бесконечных возрастающих цепей, которые для
ВВЕДЕНИЕ
9
краткости названы С-шкалами. Классом всех С-шкал характеризуется известная логика Dum. Примерами С-шкал являются частично упорядоченные шкалы с обрывом возрастающих цепей, натуральные и целые числа с естественным порядком, имеется много других примеров. Доказана теорема 1.5.4 об определимости конечным числом формул наименьших неподвижных точек позитивных П-операторов в С-моделях. Приведен алгоритм построения этих формул. Пример 1.5.10 показывает, что, вообще говоря, нельзя обойтись одной
11-формулой. Для позитивных П-операторов с несколькими аргументами доказана аналогичная теорема 1.5.13 об определимости наименьших неподвижных точек.
После этого рассмотрены строго частично упорядоченные шкалы с условием конфинальности бесконечных возрастающих цепей, которые названы SC-штлами. Классом всех SC-шкал характеризуется известная логика K4Z. Доказана теорема 1.5.19 об определимости наименьших неподвижных точек позитивных П-операторов, аналогичная теореме 1.5.4.
Видим, что имеется три типа определимости наименьших неподвижных точек позитивных П-операторов на классах моделей:
1) определимость одной П-формулой, как, например, в строго частично упорядоченных моделях с обрывом возрастающих цепей или частично упорядоченных моделях с обрывом возрастающих цепей,
2) определимость конечным числом П формул, как, например, в С-моделях и SC-моделях,
3) примеры показывают, что в конечных моделях нельзя обойтись конечным числом Il-формул, поэтому здесь мы имеем определимость бесконечным числом Г1-формул.
Во второй главе исследуются позитивные операторы общего вида, которые могут содержать П и 0- В первом параграфе рассматриваются формулы, содержащие только 0- Волее точно, модальной S-формулой называем формулу, составленную с помощью связок А, V, 0 из формул, не содержащих ни П, ни 0- Установлено, что в смысле определимости наименьших неподвижных точек S-операторы ведут себя гораздо лучше, чем П-операторы. Наименьшая неподвижная точка определима в транзитивных моделях и при этом определяющая формула получается итерацией исходной формулы и поэтому сохраняет позитивность параметров (теорема 2.1.1).
Во втором параграфе рассмотрены позитивные операторы на моделях с обрывом возрастающих цепей. Разработана конструкция опровергающих конфигураций для случая позитивных операторов. Доказано, что для любого пози-
ВВЕДЕНИЕ
10
тивного оператора существует сохраняющая позитивность Л. и параметров формула и>, определяющая наименьшую неподвижную точку этого оператора во всех строго частично упорядоченных моделях с обрывом возрастающих ценой и всех частично упорядоченных моделях с обрывом возрастающих цепей (следствие 2.2.22). Т.е. в отличие от П-формул, можно построить общую определяющую формулу для этих классов моделей.
В третьем параграфе расширены классы моделей, в которых наименьшие неподвижные точки позитивных операторов определимы с сохранением позитивности параметров. Введено понятие шкалы со слабым условием конфи-нальности бесконечных возрастающих цепей. Сначала рассмотрены частично упорядоченные шкалы с условием слабой конфинальности бесконечных возрастающих цепей, которые названы Е-шкалами. Класс 2£-шкал расширяет класс С-шкал. Логика, характеризуемая классом всех Е-шкал обозначена 84Е. Оказалось, что эта логика совпадает с логикой Г(1пСш, 1) из классификации, введенной в [4]. В [7] доказано, что Г(1пА,ш,1) обладает интерполяционным свойством Крейга. Аксиоматизация этой логики следующая
Б4Е = Б4 © □(□(/? -»Шр) -»р) -»(ОООр р).
С помощью опровергающих конфигураций доказана теорема 2.3.2 об определимости наименьших неподвижных точек позитивных операторов в ^-моделях. Особенностью доказательства является то, что конструкция из теоремы 2.2.2 применяется без изменений, но к измененной формуле. Определяющая формула сохраняет позитивность параметров. Для позитивных операторов с несколькими аргументами доказана аналогичная теорема об определимости наименьших неподвижных точек.
После этого рассмотрены строго частично упорядоченные шкалы с условием слабой конфинальности бесконечных возрастающих цепей, которые названы 5Е-шкалами. Для 5^-моделей получены аналогичные результаты. Класс б’Е-шкал расширяет класс б’С-шкал. Логика, характеризуемая классом всех Ь'Е-шкал обозначена K4.Se. Для этой логики найдена аксиоматизация.
К4Эе = К4 ф □(□/? —► р) —>(□$□?-> Пр).
В четвертом параграфе введен класс моделей, который включает в себя все £-модели и вЕ-модели. Наименьшие неподвижные точки позитивных операторов определимы в моделях введенного класса, но, вообще говоря, без сохранения позитивности параметров. Эти модели названы /ЯЕ-моделями. Они выглядят так же как Е-модели и £>£’-.модели, по в них могут одновременно
ВВЕДЕНИЕ
11
входить рефлексивные и иррефлексивныо элементы. Условие состоит в том, что рефлексивные находятся выше иррефлексивных, более точно - рефлексивные элементы образуют верхний конус. Кроме 2?-моделей и 5 £-моде л ей легко построить другие примеры ШЕ-шкал, соединив в одной шкале |>ефлексивные и иррефлексивные элементы. Доказана теорема 2.4.4 об определимости наименьших неподвижных точек позитивных операторов в 1ЯЕ-моделях. Пример 2.4.1 показывает, что определяющая формула, вообще говоря, не сохраняет позитивность параметров. В этом примере указаны 22-модель, 522-модель и позитивный оператор такие, что нельзя построить общую определяющую формулу для этих моделей, сохраняющую позитивность параметров. Здесь мы видим отличие от моделей с обрывом возрастающих цепей (см. следствие 2.2.22).
На классе всех /Л22-моделей позитивность не совпадает с монотонностью. Доказано, что формула □(□(□<? —»</) —»<?) монотонна в /2222-моделях, но не эквивалентна в классе I/222-моделей никакой позитивной но <? формуле.
Логика, характеризуемая классом всех /2222-шкал обозначена К41ге. Для этой логики найдены аксиомы.
К41ге = К4 ф □(□(р -» Пр) —> р) -> (П<Юр -> Пр) ф
□(□(р V (?) -э р) -э- (□(□(□^ -> я) -> я) -> р).
Для позитивных операторов с несколькими аргументами доказана аналогичная теорема об определимости наименьших неподвижных точек. Так как позитивность параметров не сохраняется, то метод исключения неизвестных не проходит, поэтому доказательство проведено обобщением опровергающих конфигураций на случай нескольких переменных.
Таким образом, обнаружена интересная зависимость определимости от расположения рефлексивных и иррефлексивных элементов. Этим отличаются 22-модели, 5Л’-модели и IНЕ-модели.
1) Если все элементы рефлексивны, т.е. в случае 22-моделей, то можно построить определяющую формулу, сохраняющую позитивность параметров.
2) Если все элементы иррефлексивны, т.е. в случае 522-моделей, то также можно построить о п редел я ю ту ю формулу, сохраняющую позитивность пара-МСТ)Х)В. При этом не всегда можно построить обшую для этих двух случаев определяющую формулу, сохраняющую позитивность параметров.
3) В случае /2222-моделей, когда рефлексивные элементы находятся выше иррефлексивных, определяющая формула существует, но не всегда сохраняет позитивность параметров.
4) Пример 1.2.6 показывает, что при расположении рефлексивных элементов
ВВЕДЕНИЕ
12
ниже иррефлексивных не всегда существует определяющая формула.
Зазор между /2-моделями и контрпримерами к определимости с сохранением позитивности невелик. То же относится и 5Ъ-моделям. Чуть пошире зазор между 1ЛЕ-моделями и контрпримерами к определимости. Предложен класс /ЯР-моделей, расширяющий класс /ЯР-моделей, и поставлен вопрос об определимости в этом классе.
В пятом параграфе исследуются предупорядоченные модели. Наименьшие неподвижные точки позитивных операторов могут быть не определимы в таких моделях. Доказана определимость наименьших неподвижных точек позитивных операторов на некотором классе предупорядоченных моделей (теорема 2.5.1). При этом определяющая формула получается итерацией исходной формулы и поэтому сохраняет позитивность параметров. Из этого результата получены интересные следствия 2.5.10 для логики Б4 и 2.5.11 для интуиционистской пропозициональной логики. Последнее следствие также вытекает из приведенного в конце параграфа результата В.Руитенбурга '60].
В шестом параграфе изучаются негативные операторы. Эти операторы тесно связаны с позитивными, так как квадрат негативного оператора является позитивным оператором. Негативные операторы не всегда имеют неподвижную точку. Приведен пример 2.6.5, в котором негативный оператор имеет две неподвижные точки. Среди неподвижных точек позитивного оператора имеются две особенные — наименьшая и наибольшая. Среди неподвижных точек негативного оператора трудно выделить особенные, поэтому имеет смысл сосредоточиться на случае, когда неподвижная точка единственна. Упомянутый пример показывает, что для единственности неподвижной точки нужно наложить ограничения на модели или формулы. Сначала наложено ограничение на модели — введены модели с сильным условием обрыва возрастающих цепей. Указана связь между неподвижными точками негативного оператора и его квадрата, а именно, доказана теорема 2.6.9 о том, что негативный оператор имеет неподвижную точку в модели с сильным условием обрыва возрастающих цепей тогда и только тогда, когда в этой модели неподвижная точка его квадрата единственна. В этом случае неподвижные точки этих операторов совпадают. Отсюда получаем следствие 2.6.11 утверждающее, что если в модели с сильным условием обрыва возрастающих цепей неподвижная точка негативного оператора существует, то неподвижная точка единственна. Пример 2.6.12 показывает, что для определимости нужно наложить дополнительные условия. Наложим условие транзитивности. Логика, характеризуемая к лассом всех транзитивных шкал с сильным условием обрыва возрастающих цепей,
ВВЕДЕНИЕ
13
обозначена С гг!. Найдена аксиоматизация этой логики.
Оггч = К4 ф □(□(;> -+ □/>) -> р) —> Пр.
Доказано, что дли любого негативного оператора существует формула, определяющая неподвижную точку этого оператора во всех транзитивных моделях с сильным условием обрыва возрастающих цепей, в которых неподвижная точка существует (теорема 2.6.15). Оказывается, конструкция Дж. Самбина [63] для теоремы о неподвижной точке и в этом случае дает определяющую формулу. Далее для единственности неподвижной точки наложено ограничение на формулы. Указан класс формул такой, что если соответствующий оператор имеет неподвижную точку в транзитивной модели, то эта точка единственна и определима.
В третьей главе исследуются временные позитивные Н-опораторы. В формулах вместо □ используются □ I и Од, которые имеют смысл ’’всегда было” и ’’всегда будет”. Примеры показывают, что конечности моделей недостаточно для равномерной определимости и нужно накладывать дополнительные условия. В этих примерах неограниченно увеличивается ширина модели. Поэтому рассматриваются самые узкие модели — линейные. Сначала рассмотрены конечные линейно упорядоченные модели. Доказана теорема 3.1.5 об определимости наименьших неподвижных точек позитивных 11-операторов в конечных линейно упорядоченных моделях. Аналогичная теорема 3.1.17 доказана для конечных строго линейно упорядоченных моделей. Пример 3.1.20 показывает, что общую для этих двух случаев определяющую П-формулу не всегда можно построить.
Далее рассмотрены бесконечные модели: основанные на целых числах с естественным линейным и строгим линейным порядком, на натуральных с естественным линейным и строгим линейным порядком. Во всех случаях доказаны теоремы об определимости наименьших неподвижных точек позитивных П-операторов конечным числом П-формул с сохранением позитивности параметров. Приведены примеры, показывающие, что, вообще творя, нельзя обойтись одной П-формулой. Для позитивных П-операгоров с несколькими аргументами доказаны аналогичные теоремы об определимости наименьших неподвижных точек.
Из теорем об определимости неподвижных точек вытекают следствия для соответствующих логик, аналогичные следствию 1.3.27.
По результатам диссертации были сделаны пленарные доклады на международной конференции по математической логике, посвященной 85-летию со
ВВЕДЕНИЕ
И
дня рождения А.И.Мальцева (Новосибирск, 1994), международной конференции ’’Мальцевские чтения” (Новосибирск, 1997), совместно с JI,.Л.Максимовой на международной конференции по математической логике, посвященной 90-летию со дня рождения А.И.Мальцева (Новосибирск, 1999) и доклады на конференции по нестандартным логикам и логическим аспектам информатики (Каназава, Япония, 1994), второй конференции но нестандартным логикам и логическим аспектам информатики (Иркутск, 1995), второй и третьей международных школах "Пограничные вопросы теории моделей и универсальной алгебры” (Эрлагол, 1997; Эрлагол, 1999), международной конференции но математической логике "Логика и приложения”, посвященной 60-летию со дня рождения академика Ю.Л.Ершова (Новосибирск, 2000), международной конференции ’’Мальцевские чтения” (Новосибирск, 2000). Результаты также были представлены на международных конференциях Logic Colloquium (Киль, 1993; Клермон-Ферран. 1994; Сан-Себастьян, 1996; Прага, 1998; Утрехт, 1999), 11-й межреспубликанской конференции но математической логике (Казань, 1992), 3-ей международной конференции по алгебре (Красноярск, 1993) и докладывались на совместных семинарах ИМ СО РАН и ИГУ "Нестандартные логики” и ’’Алгебра и логика”.
Основные результаты диссертации опубликованы в работах [11-18, 54, 55).
Глава 1
Позитивные П-операторы
1.1 Формульные операторы
Модальные пропозициональные формулы составляются из пропозициональной константы X (ложь) и пропозициональных переменных р, г,... с помощью бинарных связок Л и V и унарных связок -» и □. Формулы обозначаем греческими буквами а, р,... . Запись ..., уп) означает, что переменные формулы р содержатся среди <?],..., <?„. Будем также использовать унарную связку О, которая представляет собой сокращение для
Шкала Крипкс (И’Я) состоит из непустого множества И7 и бинарного отношения Я на И7. Часто для краткости будем называть шкалы Кринке просто шкалами. Если (х,у) € Я, то элемент у достижим из элемента х. Вместо (.т, у) £ Я обычно будем писать хКу.
Модель Крипке (И7, Я,?;) состоит из шкалы Кринке (И7, Я) и означивания у. Означивание V — это функция, которая каждой переменной у ставит в соответствие подмножество и(ц) множества IV. Это подмножество и(у) называется значением переменной q. Значение переменной </, будем обозначать соответствующей прописной буквой С},. Функция у естественным образом продолжается на формулы: константе X всегда соответствует пустое множество, связкам Л, V. □, 0 соответствуют дополнение, пересечение, объединение множеств и следующие операции на множествах:
ПА = {х |Уу(хЯу => у £ Л)},
0/1 = {х | 3у(хЯу Л у € -4)}.
Таким образом, значение формулы всегда является подмножеством множества ИЛ Значение формулы аг(дь... ,<?„) будем обозначать через а(<21?... ,(ЭП)* С другой стороны, означиванию соответствует функция, которая каждому зле-
15
ГЛАВА 1. ПОЗИТИВНЫЕ П ОПЕРАТОРЫ
16
менту из W сопоставляет множество переменных, истинных на этом элементе. Поэтому будем иногда говорить об означивании на элементе.
Часто для краткости будем называть модели Криике просто моделями. Модель {IV, R,v) основана на шкале {W, R).
Пусть дана формула ;р(р, 7ь..., ç,t) от переменных p,qj,... ,qn. Рассмотрим модель Кринке ( W, R,v), в которой заданы значения Qit...,Qn переменных 7t. • ■ • » Яш а значение переменной р не задано. Формула <p(p,qit..., qn) определяет на модели Крипке ( W, R, v) оператор FV(P) = <p(P,Qi,... ,Qn). который каждому множеству Р сопоставляет множество ip(P, Qi,..., Qn)- Т.е. переменной р придается значение Р и рассматривается значение формулы при этом означивании. Такие операторы назовем формульными. Переменные q\qn будем называть параметрами этого формульного оператора Fv.
Пусть дана шкала {WJÏ). Рассмотрим оператор F, не обязательно формульный, который каждому подмножеству А множества W сопоставляет некоторое подмножество F (А) множества W. Множество Р называется неподвижной тонкой оператора F, если выполняется Р = Р(Р). Таким образом, неподвижная точка формульного оператора Fv является решением уравнения Р = <p(PtQi,.. .,Qn). Неподвижная точка Р называется наименьшей неподвижной точкой оператора F, если для любой другой неподвижной точки Р' этого оператора выполняется PCP'. Неподвижная точка Р называется наибольшей неподвижной точкой оператора F, если для любой другой неподвижной точки Р' этого оператора выполняется Р'СР.
Если неподвижная точка F совпадает в модели со значением некоторой формулы u>(qi,... ,7»,), то эта формула и определяет неподвижную точку Р в данной модели. Называем эту формулу определяющей.
Вхождение переменной или константы в формулу называется
1) модализованным, если это вхождение находится под действием □ или О,
2) позитивным, если это вхождение находится под действием четного числа отрицаний (это число может быть равно нулю),
3) негативным, если это вхождение находится под действием нечетного числа отрицаний.
Если каждое вхождение переменной р в формулу ip(p, Çi,... ,qn) модализо-ванное, то назовем эту формулу модализоваппой но переменной р, а оператор Fç назовем мобилизованным. Если каждое вхождение переменной р в формулу <p(p,Çi,... ,7п) позитивное, го назовем эту формулу позитивной по р, а оператор Fф назовем позитивным.
Модальной П-формулой назовем формулу, составленную с помощью связок
І ЛАПА 1. ПОЗИТИВНЫЕ П-ОПЕРАТОРЫ
17
Л, V, □ из формул, но содержащих ни □, ни 0- Если формула ... ,</п)
является 11-формулой, то оператор называем П-оператором. Модальной £-формулой назовем формулу, составленную с помощью связок Л, V, 0 из формул, не содержащих ни □, ни О- Если формула <^(р, </і,..., цп) является Е-формулой, го оператор называем Т,-оператором.
Определяющая формул а ы (^ь... ,дп) сохраняет позитивность параметров, если для любого параметра цг выполняется следующее условие: если формула <р(р, ди — Яп) не содержит негативных вхождений параметра то и формула ^(<7ь •••><?») не содержит негативных вхождений яг. Определяющая формула ^(<?ь• • • »<7л) сохраняет позитивность X, если выполняется следующее: если формула <р(р, <7ь • • •,Яп) не содержит негативных вхождений X, то и формула .. ,<7П) не содержит негативных вхождений X.
Приведем начальные общие сведения об операторах и их неподвижных точках. Об этом молено прочитать, например, в (58, 23, 38].
Оператор F называется монотонным, если для любых А и А! из АСА' следует ^(Л)СР(Л'). Покажем, что монотонный оператор всегда имеет наименьшую и наибольшую неподвижные точки. Рассмотрим оператор Я и последовательность множеств в шкале ( И’, Я)
Р° = 0,
рШ = р(рк^
к — натуральное. Если оператор монотонный и шкала конечная, то нетрудно показать, что эта последовательность стабилизируется на наименьшей неподвижной точке этого оператора. Продолжим последовательность Рк по ординалам
раю =
для предельного Ос положим
р° = и р1>■
0<а
Предложение 1.1.1 Если оператор монотонный, то и любой модели последовательность множеств Ра стабилизируется на наименьшей неподвижной точке этого оператора.
Доказательство Последовательность Ра стабилизируется на неподвижной точке. Индукцией по а нетрудно установить, что Ра содержится в любой неподвижной точке данного оператора. Д
ГЛАВА 1 ПОЗИТИВНЫЕ Г1 -ОПЕРАТОРЫ
18
Символ Л обозначает конец доказательства, примера и т.п.
Рассмотрим последовательность множеств
.9° = И/,
= ^(5*).
В конечных моделях эта последовательность стабилизируется на наибольшей неподвижной точке. Продолжим эту последовательность по ординалам
5ой - ^(5“),
для предельного а положим
5" = Р| 5/?.
Р<а
Получим последовательность, стабилизирующуюся на наибольшей неподвижной точке в любой шкале.
Следующее предложение дает другую характеризацию наименьшей неподвижной точки монотонного оператора.
Предложение 1.1.2 Если Р - наименьшая неподвижная точка монотонного оператора Р, то Р = ПМ | Р(А)СА).
Доказательство Пусть Р(А)СА. Определим последовательность множеств
А<*+1 =
для предельного а положим
А” = р| А».
0<(х
Легко проверить, что эта последовательность — невозрастающая. Поэтому она стабилизируется на некоторой неподвижной точке. Эта точка содержит Р. Поэтому А содержит Р. Включение в другую сторону очевидно. Л
Легко понять, что позитивный оператор является монотонным, поэтому всегда имеет наименьшую и наибольшую неподвижные точки.
Определим последовательность формул
/(дь...,4«) = Д
ГЛАВА 1. ПОЗИТИВНЫЕ П-ОПЕРАТОРЫ
19
Ясно, что для всех к множество Рк является значением формулы уЛ Если <р позитивна но р и для некоторого к выполняется Рк = Рк+1 (например, так всегда бывает в конечной модели), то Рк является наименьшей неподвижной точкой оператора и определяется формулой >рк, которая сохраняет позитивность _1_ и параметров.
В оставшейся части соберем некоторые распространенные обозначения и определения.
Формула а истинна на элементе х модели, если элемент х принадлежит значению формулы о, в этом случае пишем х (= о. Формула а ложна на т, если х не принадлежит значению формулы а, в этом случае пишем х V- а. Формула а истинна в модели (И7,Я,и), если а истинна на каждом элементе модели. Формула а общезначима на шкале (Иг, Я) если а истинна в каждой модели (XV, Я,у), основанной на этой шкале.
Рассмотрим модель {\¥, Я,а) и множество V С ИЛ Подмоделью, основанной на множестве V', назовем модель (КЯ',г/), в которой И' является ограничением Я на V и у'((р) = и((]г) П V для всех i. Если для некоторого элемента I € IV подмодель основана на множестве V = {т 11 = х или то подмодель { V, ЯЛ Р) назовем порожденной подмоделью модели (И’. Я, V} или подмоделью, порожденной элементом t.
Будем использовать обозначения
Т = -»1,
□а = а Л □<*, фа = а V Оа,
= -'а V /3, аеэ-0 = (а —>0) Л ((5-> а),
□°а = а,
□п+1а = ООГа.
Можно определить последовательность формул аналогичную рк, начиная с Г. Для всех натуральных к множество 5^ будет значением соответствующей формулы. Тогда, например, для (р позитивной но р в конечной модели наибольшая неподвижная точка будет определяться соответствующей формулой.
Пусть Л/ — некоторый класс моделей Крипке. Формулы о и 0 эквивалентны на этом классе, если их значения в любой модели этого класса совпадают. Если понятно, о каком классе идет речь, то просто говорим что эти формулы
ГЛАВА 1. ПОЗИТИВНЫЕ П-ОПЕРАТОРЫ
20
эквивалентны и пишем а —/1 Например, на классе всех моделей Кринке
а V в— -(-о Л -*/?),
-Т-1,
□ (аЛД г^ □л Л □/?,
0(а V /?) - Оа V 0,3.
Пользуясь этим можно выносить Л наружу из □, а V из О-
Формулой с тесными отрицанил.ии называется формула, в которой отрицания стоят только перед переменными или константами. Ясно, что всякая <|юрмула эквивалентна формуле с тесными отрицаниями.
Подмножество К С XV называется нижним конусом, если Ух, у((хЯу А у € К) => х 6 К) и называется верхним конусом, если Ух, у((хЯу Л х € К) => у € К).
Элемент х шкалы называется рсфлекеивньш, если выполняется хЯх. Элемент х шкалы называется иррефлексивпым, если не выполняется хЯх. Элемент у накрывает элемент х или является накрытием элемента х, если х ф у и :гЯу и не су шествует элемента г такого, что х ф г фу и хЯгЯу.
Отношение Я на множестве И' называется
1) рефлексивным, если для любого х € XV выполняется хЯх,
2) иррефлексивпым, если для любого х € XV не выполняется хВ.х,
•3) транзитивным, если для любых х, у, г (5 IV из хЯу и у Яг следует хКг,
4) симметричным, если для любых т, у 6 XV из хЯу следует уЯх,
5) антисимметричным, если для любых х,у € XV из хЯу и уЯх следует
х-У,
6) линейным, если дня любых различных х,у 6 XV выполняется хЯу или
у Яг.
Множество (XV, Я) с бинарным отношением Я называется линейным, если отношение Я. является линейным.
Отношение Я называется предпо])ядком, если Я рефлексивно и транзитвно. В этом случае вместо Я, обычно пишем С Множество (XV, ^) называется предупорядоченным.
Отношение Я называется частичным порядком, если Я рефлексивно, тран-зитивно и антисимметрично. В этом случае также вместо Я обычно пишем Множество (XV, ^) называется частично упорядоченным. Если отношение ^ линейно, то оно называется линейным порядком., а множество {И’, ^) линейно упорядоченным.
ГЛАВА 1. ПОЗИТИВНЫЕ II-ОПЕРАТОРЫ
21
Отношение Я называется строгим частичным порядком, если Я иррефлек-сиопо и транзитивно. В этом случае вместо И пишем <. Множество { И’, <} называется строго частично упорядоченным, Если отношение < линейно, то оно называется строгим линейным порядком, а множество {\\\ <) — строго линейно упорядоченным.
Каждому строгому частичному порядку < соответствует частичный порядок ^ определяемый так: х ^ у тогда и только тогда, когда х = у или .т < у. Обратно, каждому частичному порядку < соответствует строгий частичный порядок: х < у тогда и только тогда, когда х ^ у и х ^ у.
Шкала (И7 Я) является шкачой с обрывом возрастающих цепей, если в ней не существует бесконечной последовательности XI, Х2,- - такой, что все х, различны и х,Ихц1 для всех г > 1. Модель {И7. Я,г;) является моделью с обрывом возрастающих цепей, если она основана на шкале с обрывом возрастающих ценой. Ясно, что все конечные шкапы являются шкапами с обрывом возрастающих цепей.
Отношение Я называется эквивалентностью, если Я рефлексивно, транзи-тивио и симметрично. Если отношение Я на множестве (И7, Я) транзитивно, то можно определить отношение эквивалентности на этом множестве следующим образом: элементы х и у попадают в один класс эквивалентности, если х = у или выполняется хЯу и уНх. Соответствующие классы эквивалентности называются сгустками. Различают три типа, сгустков
1) вырожденный сгусток состоит из одной иррефлексивного элемента,
2) простой сгусток состоит из одного рефлексивного элемента,
3) собственный содержит не менее двух (рефлексивных) элементов.
Транзитивные шкапы состоят из сгустков. На этих сгустках можем рассматривать соответствующие отношения ^ и <. Предупорядоченные шкалы состоят из простых и собственных сгустков.
1.2 Примеры
Здесь приведены несколько примеров наименьших неподвижных точек, не являющихся определимыми. Многие из примеров используют одну из следующих 11-формул
□р,
0(рчя),
□(р V у) V П(р V -><?).