Неподвижные точки модальных операторов тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

Введение

1 Позитивные П-операторы

1.1 Формульные операторы.

1.2 Примеры.

1.3 Строго частично упорядоченные модели с обрывом возрастающих цепей.

1.4 Частично упорядоченные модели с обрывом возрастающих цепей

1.5 Модели с условием конфинальности бесконечных возрастающих цепей

2 Позитивные операторы

2.1 Е-операторы.

2.2 Модели с обрывом возрастающих цепей

2.3 Модели с условием слабой конфинальности бесконечных возрастающих цепей.

2.4 Определимость без сохранения позитивности.

2.5 Предупорядоченные модели.

2.6 Негативные операторы.

3 Временные операторы

3.1 Позитивные П-операторы.

При любом преобразовании объектов какой-то объект может остаться неизменным. Тогда это — неподвижная точка. Так же как идея отображений, преобразований пронизывает математику, так и неподвижные точки широко встречаются во всей математике. Неподвижные точки прямо имеются в виду, когда отображение или процедура описывается рекурсивно. Определение также может быть индуктивным, в этом случае определяемое множество объектов является неподвижной точкой.

Начало исследований неподвижных точек в областях, близких к данной работе, можно отнести к 20-м годам 20-го века. Б.Кнастер и А.Тарский рассматривали неподвижные точки операторов, действующих на подмножествах некоторого множества [49]. Неподвижные точки отображений решеток исследовались А.Тарским [74, 75].

Операторы могут содержать параметры. Неподвижная точка называется определимой, если она выражается через эти параметры. При этом естественно соблюдать баланс средств, т.е. пользоваться теми же средствами, что и при составлении оператора. В исследовании неподвижных точек можно выделить два случая: неподвижные точки определимы и не определимы. В случае, когда неподвижные точки не определимы, добавление оператора неподвижной точки увеличивает выразительную силу. Если неподвижные точки определимы, то это означает, что в системе достаточно средств для их выразимости. Данная работа посвящена определимым неподвижным точкам.

В теории модальных логик имеется широко известная теорема о неподвижной точке, значение которой выходит за рамки неклассических логик. Эта теорема утверждает определимость и единственность неподвижной точки мо-дализованного оператора в модальной логике Геделя-Леба, связанной с арифметической доказуемостью. Историю доказательства теоремы можно найти в [59, 69, 71, 72]. Сначала К. Бернарди [25, 26] и К. Сморинский (анонсировано в [68]) доказали ее в частном случае. В полном виде теорему доказали Д. де Йонг (не опубликовано) и Дж. Самбин [62]. Другие доказательства этой теоремы можно найти в [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].

Вообще говоря, позитивность не всегда совпадает с монотонностью. Даже в этом случае позитивные операторы составляют важнейший подкласс монотонных. Они задаются простым, легко проверяемым синтаксическим условием позитивности. Одним из затруднений, связанным с монотонностью, является то, что монотонность может не устанавливаться алгоритмически.

Еще одна область исследований непосредственно примыкает к неподвижным точкам — это решение уравнений, так как неподвижная точка является решением уравнения особого вида. В свою очередь разрешимость уравнений тесно связана с допустимостью правил вывода. В [40] Х.Фридманом поставлена проблема №40: разрешима ли алгоритмически проблема допустимости правил вывода в интуиционистской пропозициональной логике? А.В.Кузнецовым была поставлена проблема: обладает ли эта логика конечным базисом для допустимых правил? Основные результаты в этой области получены В.В.Рыбаковым. В [20] проблема Х.Фридмана решена положительно. Найден критерий допустимости правил вывода в модальной системе 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) Доказана определимость наименьших неподвижных точек позитивных операторов в ШЕ-моделях. Класс ШЕ-моделей введен в данной работе и охватывает большую часть моделей, в которых наименьшие неподвижные точки позитивных операторов определимы. Построены контрпримеры к определимости. Они основаны на моделях, находящихся очень близко к 1НЕ-моделям.

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

3) Исследованы подклассы позитивных операторов: позитивные Е-операторы и П-операторы. Для позитивных Е-операторов доказана определимость наименьших неподвижных точек в транзитивных моделях. Для позитивных П-операторов доказана определимость конечным числом формул наименьших неподвижных точек в частично упорядоченных и строго частично упорядоченных моделях с условием конфинальности бесконечных возрастающих цепей. Обнаруженная здесь определимость конечным числом формул является весьма интересным вариантом определимости.

4) Доказано, что наименьшие неподвижные точки позитивных операторов определимы в предупорядоченных моделях с ограниченным числом перемен истинности.

5) Для негативных операторов доказана единственность неподвижных точек в моделях с сильным условием обрыва возрастающих цепей и определимость в транзитивных моделях с сильным условием обрыва возрастающих цепей.

6) Доказана определимость наименьших неподвижных точек временных позитивных П-операторов в конечных линейно упорядоченных и строго линейно упорядоченных моделях, а также в бесконечных моделях: основанных на натуральных и целых числах с естественным линейным и строгим линейным порядком.

В диссертации исследуются операторы, которые можно задать формулой в моделях Крипке. Пусть дана формула </?(р, дь ., дп). Рассмотрим модель Крипке (IV, Р, V), в которой заданы значения <2ь ., <3п переменных ., а значение переменной р не задано. Формула ср(р, <71,., дп) определяет на модели Крипке (]У, Р, V) оператор Р<ДР) = <р(Р, (¿1, ■ ■ ■, <5„), который каждому множеству Р сопоставляет множество <р(Р, <3ь • • •, Т.е. переменной р придается значение Р и рассматривается значение формулы ср при этом означивании. Такие операторы назовем формульными. Переменные <71,., <?п будем называть параметрами этого формульного оператора Р^. Если каждое вхождение переменной р в формулу <р(р, <71,., цп) позитивное, то назовем эту формулу позитивной по р, а оператор Р^, назовем позитивным. Если каждое вхождение переменной р в формулу <р(р, ., модализованное, то назовем эту формулу модализованной по переменной р, а оператор Р^, назовем мобилизованным. Модальной П-формулой называем формулу, составленную с помощью связок А, V, □ из формул, не содержащих ни □, ни О- Если формула (р(р, <71,., <7п) является П-формулой, то оператор Р^ называем П-оператором. Множество Р называется неподвижной точкой оператора Р^,, если выполняется Р = РДР).

Если неподвижная точка Р совпадает в модели со значением некоторой формулы а>(<71, • • •, <7„), то эта формула со определяет неподвижную точку Р в данной модели. Называем эту формулу определяющей. Определяющая формула о>(<71,., <7П) сохраняет позитивность параметров, если для любого параметра <7г выполняется следующее: если формула (р{р, дь ., не содержит негативных вхождений параметра то и формула а;(<71,., не содержит негативных вхождений д^. Будем использовать обозначения Иа: = аЛПа, фа = а\/0а:.

В первой главе исследуются позитивные П-операторы. Во втором параграфе приведены несколько важных примеров наименьших неподвижных точек, не являющихся определимыми.

В третьем параграфе рассмотрены строго частично упорядоченные модели Крипке с обрывом возрастающих цепей. Имеется известная теорема о неподвижной точке, принадлежащая К. Бернарди, Д. де Йонгу, К. Сморинскому и Дж. Самбину. Эквивалентная формулировка в терминах моделей такова

Теорема о неподвижной точке. Для любого модализованного оператора ^ его неподвижная точка в любой строго частично упорядоченной модели Крипке с обрывом возрастающих цепей существует и единственна и, кроме того, существует формула со, определяющая эту точку во всех таких моделях.

Доказано предложение о сведении позитивного случая к модализованному. С помощью этого предложения из теоремы о неподвижной точке получаем теорему 1.3.6, утверждающую, что в рассматриваемых моделях наименьшая неподвижная точка позитивного П-оператора определяется некоторой П-формулой, единой для всех таких моделей. При этом определяющая формула сохраняет позитивность параметров.

Далее будут рассматриваться более сложно устроенные модели, на которые упомянутая теорема о неподвижной точке не распространяется. Поэтому разработана конструкция опровергающих конфигураций, которая в дальнейшем будет использоваться для более широких классов моделей. Она также дает алгоритм построения определяющих формул. С ее помощью в этом параграфе дано другое доказательство теоремы 1.3.6. Из этой теоремы получаем следствие 1.3.27 для модальной логики Геделя-Леба СЬ. Далее рассмотрены операторы с несколькими аргументами. Для таких позитивных П-операторов доказана аналогичная теорема об определимости наименьших неподвижных точек. Важность сохранения позитивности параметров состоит в том, что оно позволяет использовать метод исключения неизвестных.

В четвертом параграфе рассмотрены частично упорядоченные модели Крипке с обрывом возрастающих цепей. На них теорема о неподвижной точке не распространяется, поэтому доказательство теоремы 1.4.1 об определимости наименьших неподвижных точек позитивных П-операторов дано с помощью опровергающих конфигураций, несколько модифицированных для данного случая. Алгоритмы построения определяющей П-формулы для строго частично упорядоченных и частично упорядоченных моделей различны. Это различие существенно, в конце параграфа приведен пример 1.4.21, показывающий, что единую для этих случаев П-формулу построить, вообще говоря, нельзя.

В пятом параграфе расширяется класс моделей, в которых определимы наименьшие неподвижные точки позитивных П-операторов. Однако, определимость здесь несколько другая. Если в моделях с обрывом возрастающих цепей было достаточно одной П-формулы, то здесь нужно конечное число П-формул. Вводится понятие шкалы с условием конфинальности бесконечных возрастающих цепей. Сначала рассмотрены частично упорядоченные шкалы с условием конфинальности бесконечных возрастающих цепей, которые для краткости названы С-шкалами. Классом всех С-шкал характеризуется известная логика Dum. Примерами С-шкал являются частично упорядоченные шкалы с обрывом возрастающих цепей, натуральные и целые числа с естественным порядком, имеется много других примеров. Доказана теорема 1.5.4 об определимости конечным числом формул наименьших неподвижных точек позитивных П-операторов в С-моделях. Приведен алгоритм построения этих формул. Пример 1.5.10 показывает, что, вообще говоря, нельзя обойтись одной П-формулой. Для позитивных П-операторов с несколькими аргументами доказана аналогичная теорема 1.5.13 об определимости наименьших неподвижных точек.

После этого рассмотрены строго частично упорядоченные шкалы с условием конфинальности бесконечных возрастающих цепей, которые названы SC-шкалами. Классом всех 5С-шкал характеризуется известная логика K4Z. Доказана теорема 1.5.19 об определимости наименьших неподвижных точек позитивных П-операторов, аналогичная теореме 1.5.4.

Видим, что имеется три типа определимости наименьших неподвижных точек позитивных П-операторов на классах моделей:

1) определимость одной П-формулой, как, например, в строго частично упорядоченных моделях с обрывом возрастающих цепей или частично упорядоченных моделях с обрывом возрастающих цепей,

2) определимость конечным числом П-формул, как, например, в С-моделях и 5С-моделях,

3) примеры показывают, что в конечных моделях нельзя обойтись конечным числом П-формул, поэтому здесь мы имеем определимость бесконечным числом П-формул.

Во второй главе исследуются позитивные операторы общего вида, которые могут содержать □ и О- В первом параграфе рассматриваются формулы, содержащие только 0- Более точно, модальной Е-формулой называем формулу, составленную с помощью связок А, V, 0 из формул, не содержащих ни □, ни 0- Установлено, что в смысле определимости наименьших неподвижных точек Е-операторы ведут себя гораздо лучше, чем П-операторы. Наименьшая неподвижная точка определима в транзитивных моделях и при этом определяющая формула получается итерацией исходной формулы и поэтому сохраняет позитивность параметров (теорема 2.1.1).

Во втором параграфе рассмотрены позитивные операторы на моделях с обрывом возрастающих цепей. Разработана конструкция опровергающих конфигураций для случая позитивных операторов. Доказано, что для любого позитивного оператора F,p существует сохраняющая позитивность J и параметров формула со, определяющая наименьшую неподвижную точку этого оператора во всех строго частично упорядоченных моделях с обрывом возрастающих цепей и всех частично упорядоченных моделях с обрывом возрастающих цепей (следствие 2.2.22). Т.е. в отличие от П-формул, можно построить общую определяющую формулу для этих классов моделей.

В третьем параграфе расширены классы моделей, в которых наименьшие неподвижные точки позитивных операторов определимы с сохранением позитивности параметров. Введено понятие шкалы со слабым условием конфинальности бесконечных возрастающих цепей. Сначала рассмотрены частично упорядоченные шкалы с условием слабой конфинальности бесконечных возрастающих цепей, которые названы Е-шкалами. Класс ¿-шкал расширяет класс С-шкал. Логика, характеризуемая классом всех ¿'-шкал обозначена S4E. Оказалось, что эта логика совпадает с логикой r(Int,a>, 1) из классификации, введенной в [4]. В [7] доказано, что r(Int,t<;, 1) обладает интерполяционным свойством Крейга. Аксиоматизация этой логики следующая

S4E = S4©D(n(p^np)-^p)->(a0Dp^p).

С помощью опровергающих конфигураций доказана теорема 2.3.2 об определимости наименьших неподвижных точек позитивных операторов в ¿-моделях. Особенностью доказательства является то, что конструкция из теоремы 2.2.2 применяется без изменений, но к измененной формуле. Определяющая формула сохраняет позитивность параметров. Для позитивных операторов с несколькими аргументами доказана аналогичная теорема об определимости наименьших неподвижных точек.

После этого рассмотрены строго частично упорядоченные шкалы с условием слабой конфинальности бесконечных возрастающих цепей, которые названы SE-шкалами. Для ¿'¿-моделей получены аналогичные результаты. Класс SE-шкал расширяет класс ¿"С-шкал. Логика, характеризуемая классом всех ¿¿-шкал обозначена K4Se. Для этой логики найдена аксиоматизация.

K4Se = К4фП(Пр^р)->(ПфПр->Ор).

В четвертом параграфе введен класс моделей, который включает в себя все ¿-модели и ¿¿-модели. Наименьшие неподвижные точки позитивных операторов определимы в моделях введенного класса, но, вообще говоря, без сохранения позитивности параметров. Эти модели названы IRE-моделями. Они выглядят так лее как ¿-модели и ¿¿-модели, но в них могут одновременно входить рефлексивные и иррефлексивные элементы. Условие состоит в том, что рефлексивные находятся выше иррефлексивных, более точно - рефлексивные элементы образуют верхний конус. Кроме Е'-моделей и ¿'Е'-моделей легко построить другие примеры ШЕ-шкал, соединив в одной шкале рефлексивные и иррефлексивные элементы. Доказана теорема 2.4.4 об определимости наименьших неподвижных точек позитивных операторов в //¡^-моделях. Пример 2.4.1 показывает, что определяющая формула, вообще говоря, не сохраняет позитивность параметров. В этом примере указаны ^-модель, 5£-модель и позитивный оператор такие, что нельзя построить общую определяющую формулу для этих моделей, сохраняющую позитивность параметров. Здесь мы видим отличие от моделей с обрывом возрастающих цепей (см. следствие 2.2.22).

На классе всех 1ЯЕ-моделей позитивность не совпадает с монотонностью. Доказано, что формула □(□(□<?—>-д) монотонна в 1ЯЕ-моделях, но не эквивалентна в классе 1ЯЕ-моделей никакой позитивной по д формуле.

Логика, характеризуемая классом всех IЯЕ-шкгл обозначена К41ге. Для этой логики найдены аксиомы.

К41ге = К4 ©□(□(? ->• Ор) р) (ПфПр ->• □ р) Ф □(□(р V ->р) (□(□(□? ->д)->д)->р).

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

Таким образом, обнаружена интересная зависимость определимости от расположения рефлексивных и иррефлексивных элементов. Этим отличаются ^-модели, БЕ-модели и 1ИЕ-модели.

1) Если все элементы рефлексивны, т.е. в случае ^-моделей, то можно построить определяющую формулу, сохраняющую позитивность параметров.

2) Если все элементы иррефлексивны, т.е. в случае 5£'-моделей, то также можно построить определяющую формулу, сохраняющую позитивность параметров. При этом не всегда можно построить общую для этих двух случаев определяющую формулу, сохраняющую позитивность параметров.

3) В случае 1Н.Е-моделей, когда рефлексивные элементы находятся выше иррефлексивных, определяющая формула существует, но не всегда сохраняет позитивность параметров.

4) Пример 1.2.6 показывает, что при расположении рефлексивных элементов ниже иррефлексивных не всегда существует определяющая формула.

Зазор между Е'-моделями и контрпримерами к определимости с сохранением позитивности невелик. То же относится и ¿'^'-моделям. Чуть пошире зазор между 1ЯЕ-моделями и контрпримерами к определимости. Предложен класс 1В.Р-моделей, расширяющий класс /Д.Е'-моделей, и поставлен вопрос об определимости в этом классе.

В пятом параграфе исследуются предупорядоченные модели. Наименьшие неподвижные точки позитивных операторов могут быть не определимы в таких моделях. Доказана определимость наименьших неподвижных точек позитивных операторов на некотором классе предупорядоченных моделей (теорема 2.5.1). При этом определяющая формула получается итерацией исходной формулы и поэтому сохраняет позитивность параметров. Из этого результата получены интересные следствия 2.5.10 для логики Б4 и 2.5.11 для интуиционистской пропозициональной логики. Последнее следствие также вытекает из приведенного в конце параграфа результата В.Руитенбурга [60].

В шестом параграфе изучаются негативные операторы. Эти операторы тесно связаны с позитивными, так как квадрат негативного оператора является позитивным оператором. Негативные операторы не всегда имеют неподвижную точку. Приведен пример 2.6.5, в котором негативный оператор имеет две неподвижные точки. Среди неподвижных точек позитивного оператора имеются две особенные — наименьшая и наибольшая. Среди неподвижных точек негативного оператора трудно выделить особенные, поэтому имеет смысл сосредоточиться на случае, когда неподвижная точка единственна. Упомянутый пример показывает, что для единственности неподвижной точки нужно наложить ограничения на модели или формулы. Сначала наложено ограничение на модели — введены модели с сильным условием обрыва возрастающих цепей. Указана связь между неподвижными точками негативного оператора и его квадрата, а именно, доказана теорема 2.6.9 о том, что негативный оператор имеет неподвижную точку в модели с сильным условием обрыва возрастающих цепей тогда и только тогда, когда в этой модели неподвижная точка его квадрата единственна. В этом случае неподвижные точки этих операторов совпадают. Отсюда получаем следствие 2.6.11 утверждающее, что если в модели с сильным условием обрыва возрастающих цепей неподвижная точка негативного оператора существует, то неподвижная точка единственна. Пример 2.6.12 показывает, что для определимости нужно наложить дополнительные условия. Наложим условие транзитивности. Логика, характеризуемая классом всех транзитивных шкал с сильным условием обрыва возрастающих цепей, обозначена Сггх- Найдена аксиоматизация этой логики.

Сггх = К4 ©□(□(?->□?) -»Пр.

Доказано, что для любого негативного оператора существует формула, определяющая неподвижную точку этого оператора во всех транзитивных моделях с сильным условием обрыва возрастающих цепей, в которых неподвижная точка существует (теорема 2.6.15). Оказывается, конструкция Дж. Самбина [63] для теоремы о неподвижной точке и в этом случае дает определяющую формулу. Далее для единственности неподвижной точки наложено ограничение на формулы. Указан класс формул такой, что если соответствующий оператор имеет неподвижную точку в транзитивной модели, то эта точка единственна и определима.

В третьей главе исследуются временные позитивные П-операторы. В формулах вместо □ используются П^ и которые имеют смысл "всегда было" и "всегда будет". Примеры показывают, что конечности моделей недостаточно для равномерной определимости и нужно накладывать дополнительные условия. В этих примерах неограниченно увеличивается ширина модели. Поэтому рассматриваются самые узкие модели — линейные. Сначала рассмотрены конечные линейно упорядоченные модели. Доказана теорема 3.1.5 об определимости наименьших неподвижных точек позитивных П-операторов в конечных линейно упорядоченных моделях. Аналогичная теорема 3.1.17 доказана для конечных строго линейно упорядоченных моделей. Пример 3.1.20 показывает, что общую для этих двух случаев определяющую П-формулу не всегда можно построить.

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

Из теорем об определимости неподвижных точек вытекают следствия для соответствующих логик, аналогичные следствию 1.3.27.

По результатам диссертации были сделаны пленарные доклады на международной конференции по математической логике, посвященной 85-летию со

ВВЕДЕНИЕ 14 дня рождения А.И.Мальцева (Новосибирск, 1994), международной конференции "Мальцевские чтения" (Новосибирск, 1997), совместно с Л.Л.Максимовой на международной конференции по математической логике, посвященной 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. Гончаров С. С., Ершов Ю. Л., Свириденко Д. И. Е-программирование // Вычислительные системы.- АН СССР. Сиб. отд-ние. Ин-т математики.-Новосибирск, 1985.- Вып. 107: Логико-математические основы проблемы МОЗ. - С. 3-29.

2. Ершов Ю. Л. Определимость и вычислимость Новосибирск: Научная книга, 1996.

3. Максимова Л. Л. Интерполяционные теоремы в модальных логиках и амальгамируемые многообразия топобулевых алгебр // Алгебра и логика. -1979.- Т. 18, № 5.- С. 556-586.

4. Максимова Л. Л. Об одной классификации модальных логик // Алгебра и логика,- 1979,- Т. 18, № 3,- С. 328-340.

5. Максимова Л. Л. Интерполяционные теоремы в модальных логиках. Достаточные условия // Алгебра и логика.- 1980.- Т. 19, № 2. С. 194-213.

6. Максимова Л. Л. Интерполяционная теорема Линдона в модальных логиках)/ Тр. Ин-та математики/ АН СССР. Сиб. отд-ние.- 1982.-Т.2:Математическая логика и теория алгоритмов.- С. 45-55.

7. Максимова Л. Л. Об интерполяции в нормальных модальных логиках)/ Математические исследования.- Кишинев, 1987.- Вып.98:Неклассические логики.- С. 40-56.

8. Максимова Л. Л. Аналог теоремы Бета в нормальных расширениях модальной логики К А / / Сибирский математический журнал.- 1992.- Т. 33, № 6,- С. 118-130.

9. Максимова Л. Л. Модальные логики и многообразия модальных алгебр: свойства Бета, интерполяция и амальгамируемость // Алгебра и логика,- 1992 Т. 31, № 2,- С. 145-166.

10. Максимова Jl. JI. Проективные свойства Бета в модальных и суперинтуиционистских логиках // Алгебра и логика.- 1999.- Т. 38, № 3.- С. 316-333.

11. Мардаев С. И. Неподвижные точки модальных схем // Алгебра и логика.1992,- Т. 31, № 5,- С. 493-498.

12. Мардаев С. И. Наименьшие неподвижные точки в логике Гжегорчика и интуиционистской пропозициональной логике // Алгебра и логика.1993.- Т. 32, № 5,- С. 519-536.

13. Мардаев С. И. Наименьшие неподвижные точки в логике Геделя-Леба // Алгебра и логика.- 1993.- Т. 32, № 6.- С. 683-689.

14. Мардаев С. И. О сходимости позитивных схем в SA и Int // Алгебра и логика,- 1994,- Т. 33, № 2.- С. 166-178.

15. Мардаев С. И. Модальные П-схемы // Алгебра и теория моделей.- Новосибирск, 1997,- С. 99-109.

16. Мардаев С. И. Негативные модальные схемы // Алгебра и логика.- 1998.Т. 37, № 3.- С. 329-337.

17. Мардаев С. И. Модальные позитивные операторы // Алгебра и логика.-1999.- Т. 38, № 5,- С. 585-597.

18. Мардаев С. И. Неподвижные точки временных операторов // Алгебра и теория моделей 2,- Новосибирск, 1999.- С. 68-77.

19. Рыбаков В. В. Допустимые правила предтабличных модальных логик // Алгебра и логика,- 1981.- Т. 20, № 4,- С. 440-464.

20. Рыбаков В. В. Критерий допустимости правил в модальной системе 54 и интуиционистской логике // Алгебра и логика.- 1984,- Т. 23, N- 5-С. 546-572.

21. Рыбаков В. В. Базисы допустимых правил логик Б4 и Int // Алгебра и логика.- 1985.- Т. 24, № 1,- С. 87-107.

22. Рыбаков В. В. Уравнения в свободной топобулевой алгебре // Алгебра и логика,- 1986,- Т. 25, № 2,- С. 172-204.

23. Barwise J. Admissible Sets and Structures Springer-Verlag, 1975.

24. Bernardi C. The fixed-point theorem for diagonalizable algebras // Studia Logica.- 1975.- Vol. 34, № 3.- P. 239-251.

25. Bernardi C. The uniqueness of the fixed-point in every diagonalizable algebra // Studia Logica,- 1976.- Vol. 35, № 4.- P. 335-343.

26. Beth E. W. On Padoa's method in the theory of definition // Indagationes Mathematicae 1953.- Vol. 15, № 4,- P. 330-339.

27. Boolos G. The Unprovability of Consistency.- Cambridge University Press, 1979.

28. Boolos G. On systems of modal logic with provability interpretations // Theoria.- 1980.- Vol. 46, № 1,- P. 7-18.

29. Boolos G. The Logic of Provability Cambridge University Press, 1993.

30. Chagrov A., Zakharyaschev M. Modal Logic Clarendon Press, 1997.

31. Craig W. Three uses of Herbrand-Gentzen theorem in relating model theory and proof theory // The Journal of Symbolic Logic 1957.- Vol. 22, № 3.- P. 269285.

32. Czermak J. Interpolation theorem for some modal logics// Logic Colloquium'73.- North-Holland Publishing Company, 1975.- P. 381-393.

33. Ebbinghaus H.-D. Extended Logics: The General Framework// Model-Theoretic Logics.- Springer-Verlag, 1985.- P. 25-76.

34. Ebbinghaus H.-D., Flum J. Finite Model Theory- Berlin, Springer-Verlag, 1995.

35. Fitting M. C. Proof methods for modal and intuitionistic logics.- D. Reidel Publishing Company, 1983.

36. Freedman H. One hundred and two problems in mathematical logic // The Journal of Symbolic Logic.- 1975.- Vol. 40, № 2,- P. 113-130.

37. Gabbay D. M. Craig's interpolation theorem for modal logics// Conference in Mathematical Logic, London, 1970 Springer-Verlag, 1972 - P. 111-127.

38. Gandy R. O. Inductive definitions// Generelized Recursion Theory.- North-Holland Publishing Company, 1974.- P. 265-299.

39. Ghilardi S. Unification and projectivity in propositional logic Milano, 1996.-(Quaderno n.58/96, Dipartimento di Matematica, Université degli Studi).

40. Ghilardi S. Best solving modal equations// Logic Colloquium, Utrecht, 1999.-P. 21.

41. Ghilardi S. Unification in intuitionistic logic // The Journal of Symbolic Logic.-1999.- Vol. 64, № 2,- P. 859-880.

42. Gleit Z., Goldfarb W. Characters and fixed points in provability logic // Notre Dame Journal of Formal Logic 1990.- Vol. 31, № 1.- P. 26-36.

43. Henkin L. An extension of the Craig-Lyndon interpolation theorem // The Journal of Symbolic Logic.- 1963,- Vol. 28, № 3,- P. 201-216.

44. Ignatiev K. N. On strong provability predicates and the associated modal logics // The Journal of Symbolic Logic.- 1993.- Vol. 58, № 1,- P. 249-290.

45. Knaster B. Un théorème sur les fonctions d'ensembles // Annales de la Société Polonaise de Mathématique.- 1927 (издано в 1928).- Vol. 6.- P. 133-134, .

46. Kozen D. Results on the propositional ц-calculus // Automata, Languages, and Programming, Ninth Colloquium.- Springer, 1982,- P. 348-359.

47. Kozen D. A Finite Model Theorem for the Propositional ¡x-Calculus // Studia Logica.- 1988.- Vol. 47, № 3.- P. 233-241.

48. Lyndon R. C. An interpolation theorem in the predicate calculus // Pacific journal of mathematics.- 1959 Vol. 9, № 1- P. 129-142.

49. Lyndon R. C. Properties preserved under homomorphism // Pacific journal of mathematics.- 1959.- Vol. 9, № 1- P. 143-154.

50. Mardaev S. I. Fixed points of modal negative operators // Bulletin of the Section of Logic.- 1997,- Vol. 26, № 3.- P. 135-138.

51. Mardaev S. I. Definability of least fixed points // Логика и приложения. Me-ждунар. конф., посвящ. 60-летию со дня рождения акад. Ю.Л.Ершова. -Новосибирск, 2000.- С. 128.

52. Montagna F. Review of "Lisa Reidhaar- Olson, A new proof of the fixed-point theorem of provability logic, Notre Dame Journal of Formal Logic 31 (1990), №1, 37-43" // The Journal of Symbolic Logic.- 1993.- Vol. 58, № 2,- P. 714715.

53. Montagna F. Review of "Zachary Gleit and Warren Goldfarb, Characters and fixed points in provability logic, Notre Dame Journal of Formal Logic 31 (1990), №1, 26-36" // The Journal of Symbolic Logic.- 1993,- Vol. 58, № 2,- P.715.

54. Moschovakis Y. N. Elementary Induction on Abstract Structures.- North-Holland Publishing Company, 1974.

55. Reidhaar-Olson L. A new proof of the fixed-point theorem of provability logic // Notre Dame Journal of Formal Logic.- 1990.- Vol. 31, № 1- P. 37-43.

56. Ruitenburg W. On the period of sequences (An(p)) in intuitionistic propositional calculus // The Journal of Symbolic Logic.- 1984,- Vol. 49, № 3,- P. 892-899.

57. Rybakov V. V. Admissibility of Logical Inference Rules.- Elsevier Science Publishers B.V., 1997.

58. Sambin G. An effective fixed-point theorem in intuitionistic diagonalizable algebras // Studia Logica.- 1976,- Vol. 35, № 4.- P. 345-361.

59. Sambin G., Valentini S. The modal logic of provability: The sequential approach // Journal of Philosophical Logic.- 1982.- Vol. 11, № 3.- P. 311-342.

60. Schumm G. F. Interpolation m S5 and some related systems // Reports on Mathematical Logic.- 1976,- Vol. 6.- P. 107-109.

61. Scott D. S., de Bakker J. A theory of programs Vienna, 1969.

62. Segerberg K. Modal logics with linear alternative relations j/ Theoria.- 1970. Vol. 36, № 3.- P. 301-322.

63. Segerberg K. An Essay in Classical Modal Logic Uppsala, 1971.

64. Smorynski C. Consistency and related metamathematical properties.- Amsterdam, 1975.- (Univ. of Amsterdam, Mathematics Institute Technical Report 75-02).ЛИТЕРАТУРА 231

65. Smorynski С. Beth's theorem and self-referential Sentences// Logic Colloquium 77.- North-Holland Publishing Company, 1977,- P. 253-261.

66. Smorynski C. The incompleteness theorems// Handbook in Mathematical Logic.- North-Holland Publishing Company, 1977.- P. 821-865, перевод: Смо-ринский К. Теоремы о неполноте// Справочная книга по математической логике.- М.: Наука, 1983.- Т. 4,-С. 9-53.

67. Smorynski С. Calculating self-referential Statements, 1: Explicit calculations // Studia Logica.- 1979,- Vol. 38, № 1,- P. 17-36.

68. Smorynski C. Self-Reference and Modal Logic. New York, Springer-Verlag, 1985.

69. Taitslin M. A. Review of "Roger C. Lyndon, An interpolation theorem in the predicate calculus, Pacific journal of mathematics 9 (1959), №1, 129-142" // The Journal of Symbolic Logic.- I960.- Vol. 25, № 3.- P. 273-274.

70. Tarski A. A fixpoint theorem for lattices and its applications. Preliminary report // Bulletin of the American Mathematical Society.- 1949.- Vol. 55, № 11,-P. 1051-1052 (опечатка исправлена в № 12 на стр.1192).