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

• Автор: Мардаев, Сергей Ильич
• Шифр специальности: 01.01.06
• Научная степень: Докторская
• Год защиты: 2001
• Место защиты: Новосибирск
• Количество страниц: 237 с. : ил

Оглавление
Введение

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].
Вообще говоря, позитивность не всегда совпадает с монотонностью. Даже в этом случае позитивные операторы составляют важнейший подкласс монотонных. Они задаются простым, легко проверяемым синтаксическим условием позитивности. Одним из затруднений, связанным с монотонностью, является то, что монотонность может не устанавливаться алгоритмически.
Еще одна область исследований непосредственно примыкает к неподвижным
ГЛАВА 1. ПОЗИТИВНЫЕ П-ОПЕРАТОРЫ

Лемма 1.3 ЛЗ Пусть в строго частично упорядоченной модели {IV. <, у) задано некоторое значение переменной р и выполняется х ¥ (). Пусть существует элемент у > х, максимальный среди тех, на которых ложна 9{. Тогда существует отображение / полного дерева для 9(, удовлетворяющее лемме 1.3.12, такое, что для любого ответвляющего элемента Д выполняется /(Д) > у, следовательно /(Д) (=
Доказательство Рассмотрим полное дерево для 91 и отображение д из леммы 1.3.12 для элемента у ¥ Положим, что / отображает ^ в I, а на остальных элементах полного дерева совпадает с д. Они отображаются выше у, следовательно, на них истинна 9[. Д
Сначала разберем один специальный случай.
Лемма 1.3.14 Если каждая формула 9{ содержит р, то в любой строго частично упорядоченной модели с обрывом возрастающих цепей наименьшая неподвижная точка определяется формулой Т.
Доказательство Пусть, напротив, в модели существует элемент х, не лежащий в наименьшей неподвижной точке Р. На элементе х ложна некоторая 9. Так как 91 содержит р под действием □, то существует элемент у > х, на котором ложна р, т.е. у $ Р. Продолжая, получим бесконечную возрастающую цепь. Противоречие. Д
Эта формула Т сохраняет позитивность параметров, но, вообще говоря, не сохраняет позитивность Т. Далее предполагаем, что существует формула 9[, не содержащая р. Можем считать, что она одна. Тогда существует одно полное дерево без ответвляющих элементов. Такое дерево состоит из одного элемента.
Опровергающей структурой назовем любое дерево с иррефлексивным и, вообще говоря, не транзитивным отношением 5 и приписанными формулами, которое можно построить следующим образом.
Построение 1.3.15 Возьмем полное дерево для некоторой формулы в{. Назовем его начальным деревом структуры. Рассмотрим ответвляющий элемент Д этого дерева. Возьмем экземпляр полного дерева для некоторой 0 и прикрепим этот экземпляр к элементу Д. Это означает, что элемент в[ этого экземпляра и Д отождествляются. Объединяем отношения.
Припишем элементу, полученному отождествлением в и Д, формулу и формулу, приписанную Д. Проделаем такие прикрепления ко всем ответвляющим элементам полного дерева для в, при этом к различным элементам можем