Содержание к диссертации
Введение
1 Необходимые определения 16
1.1 Синтаксис и семантика 16
1.2 Классы сложности 22
2 Основной результат 25
2.1 Формулировка основного результата 25
2.2 Модальные логики 26
2.2.1 Сложность проблемы разрешения в полном языке: вспомогательная конструкция 26
2.2.2 Сложность константного фрагмента логики К4 . 31
2.2.3 Интервал [К, К4] 36
2.2.4 Сложность фрагмента от одной переменной логики S4 37
2.2.5 Интервалы [К4, GL] и [К4, Grz] 41
2.2.6 Некоторые замечания и следствия 43
2.3 Базисная и формальная логики Виссера 44
2.3.1 Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
2.3.2 Сложность проблемы разрешения константного фрагмента логики BPL 48
2.3.3 Сложность проблемы разрешения фрагмента от одной переменной логики FPL 53
2.3.4 Некоторые замечания и следствия 58
2.4 Суперинтуиционистские логики 59
2.4.1 Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
2.4.2 Полшюмиальное погружеіше позитивного фрагмента Int в позитивный фрагмент Int с двумя переменными 61
2.4.3 Интервал [Int, КС] 70
2.4.4 Некоторые следствия 70
2.4.5 Некоторые сложностные аспекты фрагмента от двух переменных; логики КС 73
2.4.6 Обобщения и замечания 79
3 Анализ полученных результатов 82
3.1 Функция сложности 82
3.1.1 К истокам задачи 83
3.1.2 Оценка функции сложности в случае конечного числа переменных в языке 85
3.2 Комментарий 86
Библиография 91
- Классы сложности
- Сложность проблемы разрешения в полном языке: вспомогательная конструкция
- Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
- К истокам задачи
Введение к работе
Актуальность темы. При изучении той или иной логической системы или класса систем исследуются очень разные свойства; круг вопросов, относящихся к алгоритмическим аспектам таких исследований, находится на одном из первых мест. Это объясняется не только чисто теоретическим интересом к алгоритмической выразительности того или иного формального языка, но и возможностью использования полученных результатов в приложениях в информатике, теоретическом программировании и т.д. .
В XX веке было получено много результатов, связанных с алгоритмическими свойствами как классических, так и неклассических логик, причём в языках разных порядков и во многих случаях с рядом ограничений на используемые средства этих языков. Опишем ситуацию с іштересующими нас аспектами алгоритмической проблематики в отношении пропозициональных логик.
Почти все1 стандартные пропозициональные логики разрешимы (см., например, [5]). Но разрешимость той или иной логики означает лишь наличие принципиальной возможности выяснять факт принадлежности формул этой логике, и когда разрешимость обоснована, встаёт проблема поиска оптимального алгоритма, решающего вопрос о принадлежности формул данной логике. Как правило, из доказательства разрешимости удаётся извлечь лишь такие разрешающие алгоритмы, время работы которых ограничено снизу экспонентой. Естественный вопрос в каждом из таких случаев: а нет ли более быстрого — например, полиномиального по затратам времени — алгоритма разрешения? 1 Исключение составляют, например, релевантные логики, см. [24].
Одним из первых результатов в этом направлении является теорема Кука: проблема выполнимости булевых формул NP-полна [6]. Из теоремы Кука следует, что если P^NP, то классическая логика высказываний не является полиномиально разрешимой.
Хотя для многих стандартных логик оценки для верхних границ размера коитрмоделей были получены довольно давно, предметом специальных исследований сложность неклассических логик стала только в конце XX века. Дело в том, что получение таких оцепок являлось, как правило, лишь промежуточным этапом на пути доказательства разрешимости соответствующих логик, и вопросы сложности при этом не рассматривались. Вопросы о сложности неклассических (точнее, суперинтуиционистских) логик впервые были явно сформулированы А.В.Кузнецовым, см. [13]. Одной из проблем, поставленных А. В. Кузнецовым, была проблема полиномиальной эквивалентности интуиционистской и классической логик. Тот факт, что классическая логика сводится полиномиально к интуиционистской, следует из теоремы Гливенко [9]. А.В.Кузнецов показал [32], что если интуиционистская логика является полиномиально аппроксимируемой шкалами Крипкс, то она полиномиально сводится к классической, и тем самым эти логики полиномиально эквивалентны. Как следует из идей, изложенных в [32], ситуация со многими стандартными модальными логиками аналогична. Оставалось лишь обосновать полиномиальную аппроксимируемость интуиционистской логики шкалами Крипке.
Вопрос о полиномиальной аппроксимируемости интуициоігастской логики шкалами Крипкс был решён в конце 70-х годов XX века М. В. Захарьящевым. В своих работах М. В. Захарьящев рассматривал следующую функцию сложности /і,(ті), определяемую для логики L: /l(") = max min |5|, где |5| — число миров в шкале Крипке $, а \<р\ — длина формулы
Примерно в это же время Р. Ладнер [14] доказал PSPACE-полноту проблемы разрешения для модальных логик К, Т и S4 и почти сразу Р. Стэтман [20] доказал PSPACE-полноту проблемы разрешения для Int. Таким образом, положительный ответ на вопрос А. В. Кузнецова означал бы, что NP = PSPACE, более того, справедливо и обратное: если NP — PSPACE, то интуиционистская и классическая пропозициональные логики полиномиально эквивалентны.
Как Р. Ладнер, так и Р. Стэтман использовали в доказательствах PSPACE-полноты формулы в языках, содержащих бесконечно много переменных; то же можно сказать и об опубликованных позже доказательствах PSPACE-трудности проблемы разрешения тех или иных логик (см., например, [1], [5], [11], [27], [43]). Тем не менее, прикладные задачи не требуют неограниченного числа переменных в языке: как при постановке, так и при решении каждой прикладной задачи используется лишь конечное число элементарных выражений, для описания которых достаточно, конечно же, конечного числа переменных. Более того, даже язык без переменных представляет определённый интерес: поскольку формулы являются лишь схемами высказываний, то, решив ту или иную проблему для логики в целом, разумно посмотреть, как это решение соотносится со множеством самих высказываний, а типичными высказываниями можно считать как раз константные формулы. Таким образом, вполне естественно рассматривать фрагменты логик в языке с копечным числом переменных, и в [5] сформулирована соответствующая проблема (проблема 18.4):
Легко показать, что Int 6 языке с одной переменной является линейно аппроксимируемой шкалами Крипкс. Является ли Int о языке с двумя переменными линейно (или полиномиально) аппроксимируемой шкалами Крипке? Верно ли, что эта логика полиномиально разрешима? Какова ситуация с S4, Grz и другими стандартными модальными логиками в языке с одной переменной?
Имеется ряд аргументов для ожидания как положительных, так и отрицательных ответов на поставленные вопросы. Приведём некоторые из них.
Хотя проблема выполнимости булевых формул NP-полна [б], тем не менее, для всякого натурального числа п проблема выполнимости булевых формул от п переменных находится в классе Р. То же верно и для булевых формул с кванторами: проблема выполнимости булевых формул с кванторами (в полном языке) PSPACE-полна (см. [21]), но для любого п проблема выполнимости булевых формул с кванторами от п переменных находится в классе Р.
Аналогичный факт справедлив для всех локально табличных логик2: проблема разрешения их фрагментов в языке от п переменных находится в классе Р.
Проблема выводимости в Int формул от одной переменной находится в классе Р, что следует из конструкции И. Нишимуры [15].
Проблема разрешения константного фрагмента модальной логики S4 находится в классе Р; это справедливо и для расширений S4, причём имеющих сколь угодно сложную проблему разрешения и даже для неразрешимых.
Как отмечалось выше, доказательства PSPACE-полноты проблемы разрешения неклассических логик были получены в случае языка с бесконечным числом переменных; то же относится к упомянутым результатам М. В.Захарьящева. При этом для любого п фрагменты соответствующих логик, состоящие из формул от не более чем п переменных, использовавшихся Р. Ладнером и Р. Стэтманом для обоснования PSPACE-трудности, полиномиально разрешимы, поскольку они моделируют в этих логиках проблему выполнимости булевых формул с кванторами в языке с конечным числом переменных. Более того, в доказательстве Р. Стэтмана PSPACE-полноты проблемы разрешения Int использовались лишь связки Л и —У, а проблема разрешения соответствующего фрагмента Int в языке с конечным числом переменных находится в классе Р. 2Формулы ifi и т]> эквивалентны в L, если ір*-їфЄЬ. Нормальная модальная или су-нерин туици они стекая логика L называется локально табличной, если для каждого п Є N имеется лишь конечное число попарно неэквивалентных в L формул от переменных Р1.---,Рп-
Примерно во второй половине 80-х годов XX века А. В. Чагровым высказывалась гипотеза о том, что интуиционистская логика и стандартные модальные логики в языке с конечным числом переменных полиномиально аппроксимируемы шкалами Крипке, в частности, полиномиально разрешимы, причём степень соответствующего полинома зависит от числа переменных в языке3.
Уже интуиционистский язык с двумя переменными достаточно выразителен: для всякой формулы без отрицания, не выводимой в Int, существует подстановка формул от двух переменных такая, что получающаяся в результате этой подстановки формула тоже не выводится в Int, см. [34]. Кроме того, четырёх переменных достаточно, чтобы построить исчисление с неразрешимым фрагментом от двух переменных [44].
Первые известные диссертанту результаты о PSPACE-трудности проблемы разрешения логик в языке с конечным числом переменных появились лишь в 90-х годах XX века. Так, Дж. Халперн показал [10], что для К, Т, S4 и некоторых полимодальных логик проблема разрешения является PSPACE-полпой в языке с одной переменной (к сожалению, работа [10] содержит ошибки в доказательстве для наиболее интересного случая — логики S4). Чуть раньше Э. Спаан доказала [19], что проблема выполнимости модальных формул полиномиально сводится к проблеме вьшолпимостп модальных формул от одной переменной; из этого результата следует, в частности, один из результатов Дж.Халперна, именно, РSPACE-полнота проблемы разрешения фрагмента от одной переменной логики К.
Ввиду сказанного, разумно поставить вопрос о сложности проблемы разрешения пеклассических логик не только в языке с одной или двумя переменными, но и в языке без переменных, т. е. о сложности проблемы разрешения константных фрагментов некоторых логик. Причём не только относительно принадлежности классам сложности, по и относительно иных мер сложности (например, относительно функции сложности). 3Эта гипотеза высказывалась на логических конференциях, но не была нигде опубликована; А. В. Чагров сообщил диссертанту об этой гипотезе лично, см. также [4].
Цель работы. Целью работы является выяснение сложности стандартных нсклассических (суперинтуїщионистских, нормальных модальных и др.) логик в языках с конечным числом переменных. Одной из центральных проблем здесь является упомянутая выше проблема 18.4 [5] и близкие к ней.
Методы исследования. Используются методы теории алгоритмов, методы теории сложности вычислений, семантические методы теории неклассических логик.
Основные результаты диссертации представлены в следующей таблице.
Ссылка [0] в этой таблице означает, что соответствующий результат получен в данной диссертации, пометка (т) означает, что соответствующий факт тривиален. Сокращение «ел.» означает «следует из». Запись «эксп.» в графе «Функция сложности» означает, что функция сложности экспоненциальна, запись «^ эксп.» — что функция сложности ограничена снизу экспоненциальной фукнцией, «полином.» — что функция сложности полиномиальна.
Результаты, приведённые в таблице, но полученные не диссертантом, включены в таблицу для полноты описания ситуации.
Научная новизна. Все результаты диссертации являются новыми.
Работами, в которых представлены близкие результаты, являются [10], [19] и [22]. Результат [19] касается только логики К, точнее, её фрагмента от одной переменной. В [10] рассматриваются модальные логики К, Т и S4 в случае одной переменной и отсутствия в языке логических констант. При этом в диссертации усилен результат [10] и [19], касающийся логики К. Это усиление состоит в том, что при наличии в языке логической константы _1_ доказана PSPACE-погаюта проблемы разрешения константного фрагмента логики К. Дано корректное доказательство утверждения [10] в случае логики S4. В [22] рассматривается только логика Гёделя-Лёба4. Полученные в [Ю], [19] и [22] результаты в отношении указанных логик являются следствиями результатов данной диссертации.
Теоретическая и практическая ценность. Результаты, полученные в диссертации, посят теоретических! характер. Они и методы их получения могут быть использованы в исследованиях алгоритмических свойств иных классов неклассических логик, в том числе и предикатных5, а также в преподавании разделов математической логики, связанных с приложениями в теоретическом программировании, информатике и т.д.
Апробация. Результаты работы докладывались на международных конференциях «Advances in Modal Logic» (Франция, Тулуза, 2002 г.), «Колмогоров и современная математика» (Москва, 2003г.), «Смирновские чтения» (Москва, 2003 г.), «Современная логика: Проблемы теории, истории 4В [22] имеется ссыпка на работу автора [3] {в соавторстве с А. В. Чагровым), причём в [3] среди прочих содержится и результат [22]; но в [22] автор отмечает, что его результат получен в 1998 году. БСм., например, [36]. и применения в науке» (Санкт-Петербург, 2002 г. и 2004 г.), «Computer Science Applications of Modal Logic» (Москва, 2005 г.). Кроме того, результаты, вошедшие в диссертацию, докладывались на семинаре по нскласси-ческой логике в МГУ (руководитель семинара — проф. В. Б. Шехтман), на семинаре по математической логике Тверского госуниверситета (руководитель — проф. А.В.Чагров), на семинаре по информационным процессам в МГУ (руководитель — проф. В. А. Любецкий), па научно-исследовательском семинаре логического центра Института философии РАН (руководитель — проф. А.С.Карпенко), на научном семинаре в секторе логики Института философии РАН (руководитель — проф. А. С. Карпенко).
Публикации. Основные результаты диссертации опубликованы в [3], [4], [17], [28], [37], [38], [39], [40], [41], [42].
Структура и объём работы. Диссертация состоит из введения, трёх глав и библиографического списка, включающего 45 наименований. Объём работы — 95 стр.
Содержание работы. Во введении обосновывается актуальность темы диссертации, формулируется цель работы, описываются методы проведения исследования. Описываются основные результаты работы и даётся обзор всех разделов диссертации.
В главе 1 даются основные определения, описывается семантика Крппке для рассматриваемых в диссертации языков, вводятся необходимые алгоритмические понятия, в частности, определяются рассматриваемые в диссертации классы сложности.
Классы сложности
Формально под алгоритмами мы будем понимать машины Тьюринга или иную эквивалентную формализацию понятия алгоритма, см. [30], [33], [35]. Фактически мы будем пользоваться интуитивным понятием алгоритма, принимая при этом тезис Чёрча-Тьюринга, состоящий в том, что всякая функция, вычислимая алгоритмически в интуитивном смысле, вычислима с помощью некоторой машины Тьюринга.
Логику L будем называть разрешимой, если существует алгоритм, выясняющий по любой формуле языка логики L, принадлежит ли эта формула логике L. В противном случае логику L будем называть неразрешимой. Если для некоторой логики L доказана её разрешимость, то встаёт проблема разрешения L, которая состоит в указании конкретного алгоритма, разрешающего эту логику. Отметим, что, как правило, проблема разрешимости и проблема разрешения решаются одновременно: доказательство разрешимости обычно содержит описание разрешающего алгоритма (или идею его построения).
Все логики, которые мы определили в разделе 1.1, являются разрешимыми (см. [5] и [26]). Нас будет интересовать сложность проблемы разрешения определённых фрагментов этих логик, которую мы будем оцешгоать через классы сложности. Определим классы сложности, которые затрагиваются в данной работе (подробнее о классах сложности см. [8], [12], [16], [21], [29]).
Поскольку нас будут интересовать лишь задачи принадлежности (не-принадлжености) формул некоторой логике, при определении классов сложности мы ограничимся только задачами такого рода, т.е. задачами вида «х X?», где X — некоторое множество слов в некотором алфавите, а х пробегает множество всех слов в этом алфавите. Обозначим через Р класс задач, решаемых детерминированными алгоритмами за полиномиальное время от длины входных данных, через NP — класс задач, решаемых недетерминированными алгоритмами за полиномиальное время от длины входных данных, через PSPACE — класс задач, решаемых недетерминированными4 алгоритмами, затрачивающими полиномиальную память от длины входных данных. Основные результаты работы, касающиеся сложности, связаны с понятием полноты задачи в классе сложности. Дадим соответствующие определения. Пусть Е — некоторый алфавит, Е — множество всех слов в этом алфавите, / — функция, определённая на Е . Функция / называется полиномиально вычислимой, если существует алгоритм, вычисляющий /, время работы которого на слове х ограничено полиномом от длины х. Говорим, что задача «х ЄI/?» полиномиально сводится к задаче «х Є L"?», если существует полиномиально вычислимая функция /, определённая на множестве всех слов алфавита языка L , такая, что для всякого 4Или детерминированными, см. [18]. слова у в алфавите языка V уеЬ = f(y)&L". Пусть С Є {P,NP,PSPACE}. Задача «xEL?» называется С-трудной, если к ней полиномиально сводится любая задача из класса С. Задача «х Є L?» называется С-полной, если она принадлежит классу С и является С-трудной. Для класса С Є {P,NP,PSPACE} определим класс соС обычным образом: соС — {«xL?» : «г Є Г?» Є С}, где L — дополнение к L во множестве всех слов алфавита языка L, т.е. x L равносильно тому, что x$.L. Под сложностью проблемы разрешения логики L будем понимать сложность проблем «ір Є L?» и « 0 L?»; при этом первую проблему будем называть проблемой принадлежности логике L, а вторую — проблемой L-выполнимости. Ясно, что если одна из этих проблем С-полна, то вторая соС-полна. Известно, что соР —Р и coPSPACE = PSPACE5, поэтому Р-полиота или PSPACE-полнота проблемы прииадлежнсти логике L равносильна, соответственно, Р-полноте или PSPACE-полноте проблемы Ь-выполнимости. В частности, мы можем говорить о PSPACE-полпоте и о PSPACE-трудности проблемы разрешеїшя, не уточняя при этом, сложность какой проблемы — принадлежности или выполнимости — имеется в виду. 5Проблема равенства классов NP и coNP открыта; обсуждение этой проблемы см., например, в [21] или в [25], Глава 2 Для пропозициональной логики L и натурального числа п обозначим через L(n) фрагмент логики L, состоящий из формул, построенных из константы і. и переменных pi,... ,рп. Основная цель данной главы — доказать следующие теоремы. ТЕОРЕМА 2.1. Пусть логика L находится в одном из следующих интервалов: [К(0),К4(0)], [K(1),GL(1)], [K(l),Grz(l)], [BPL(1),FPL(1)], [BPL+(2),KC+(2)]. Тогда проблема разрешения для L является PSPACE-трудной. ТЕОРЕМА 2.2. Пусть L — одна из следующих логик: К(0), К4(0), BPL(O), D(l), D4(l), T(l), S4(l), GL(1), Grz(l), FPL(l), Int+(2), KC(2). Тогда проблема разрешения для L является Р SPACE -полной. Доказательство этих теорем разбито на три части: сначала мы рассмотрим модальные логики, затем — базисную и формальную логики Виссера, после чего — супериытуиционистские логики.
Мы начнём с рассмотрения модальных логик, поскольку модальный язык является более гибким для описания более-менее сложных конструкций, чем интуиционистский. Сначала мы покажем, как обосновать PSPACE-трудность проблемы разрешения достаточно большого класса модальных логик (в полном языке), при этом нам важна будет возникающая при обосновании конструкция. Техническую часть некоторых доказательств мы при этом опустим, но укажем, где эти доказательства можно найти.
Сложность проблемы разрешения в полном языке: вспомогательная конструкция
Мы начнём с рассмотрения модальных логик, поскольку модальный язык является более гибким для описания более-менее сложных конструкций, чем интуиционистский. Сначала мы покажем, как обосновать PSPACE-трудность проблемы разрешения достаточно большого класса модальных логик (в полном языке), при этом нам важна будет возникающая при обосновании конструкция. Техническую часть некоторых доказательств мы при этом опустим, но укажем, где эти доказательства можно найти. После этого мы подробно рассмотрим, как свести проблему разрешения для тех или иных модальных логик в полном языке к проблеме разрешения соответствующих их фрагментов в языке с конечным числом переменных. Если L — модальная логика, то формулу р будем называть L-выполиимой, если существует модель Крипке, в которой истинны все формулы из L и при этом опровергается формула —чр (т.е. в некотором мире которой истинна формула tp).
Для обоснования PSPACE-трудности проблемы разрешения К4 нам достаточно свести к проблеме К4-выполнимости какую-нибудь PSPACE-полную проблему. В качестве такой проблемы возьмём проблему выполни мости булевых формул с кванторами, при этом можно ограничиться формулами вида p = QiPi.. QnPn p , где Qi,.. .,Qn Є {З, V}, а р — бескванторная булева формула от переменных pi,... ,рПї см. [21]. Представим требуемое эффективное преобразование булевых формул с кванторами в модальные формулы, являющееся незначительной модификацией преобразования Р. Ладнера [14] (см. также [10]). Нам понадобятся вспомогательные пропозициональные переменные рп+1, -.. ,P2n+2i которые для удобства их восприятия мы будем обозначать через go,..., gn+i- С их помощью мы будем последовательно «объяснять», что значит Q\p\, QiPi, ЗзРз и т.д. в зависимости от того, каков очередной кванторний символ Qi — Э или V. Если 2;=У, то мы должны средствами модальных формул сказать, что переменной pi следует придавать оба варианта значения истинности и при каждом проводить дальнейшие вычисления значения формулы, а если Qi = 3, то придать одно значение из двух возможных вариантов. Каждое такое «объяснение» будем называть «раскрытием» квантора.
В соответствии с определением истинности формул, начинающихся с квантора всеобщности, опишем, как нужно «раскрывать» г -ый квантор всеобщности. Нужно рассмотреть два случая — когда переменная pi принимает значение «истина» и когда pi принимает значение «ложь», что описыва ется формулой С AD.
Квантор существования «раскрывается» проще: переменная pt должна принять какое-нибудь значение, а поскольку формула р$ V — pi является тождественно истинной, то формула, описывающая «раскрытие» кванторов существования, входящих в tp, выглядит следующим образом.
Заметим, что формула р выписывается по ір за время, ограниченное полиномом от длины tp. В самом деле, не считая фиксированных частей р (типа начала qoA -qi), на выписывание формул А, В, С, D ввиду их вполне регулярного вида уйдёт времени с п2 для некоторой константы с; кроме того, нужно переписать /? , затратив для этого не более с \ip \2 тактов времени (посимвольное переписывание), где с — некоторая константа, а \tp \ — длина формулы tp .
Пусть формула tp истинна. Заметим, что истинность ip показывает, как построить нужную К4-модель. Именно, в качестве К4-шкалы берём транзитивно-рефлексивное (для определённости) дерево высоты п+ 1, ветвление которого определяется так: из мира уровня г — 1 (уровень считаем от корня, при этом сам корень находится на уровне 0) достижимы ровно два мира уровня г, если Qi — V, и достижим ровно один мир уровня г, если Q j = 3. Оценка переменных такова: Qi истинна в точности в тех мирах, уровень которых больше или равен г; если w и го — два мира уровня г, имеющие ровно одного общего предка уровня і — 1, то для одного из них полагаем, что в нём и во всех достижимых из него мирах истинна переменная РІ, а в другом и во всех достижимых из него мирах переменная pi ложна; если w и и/ — миры уровня г — 1 и і соответственно, такие, что w — единственный міф уровня г, достижимый из ги, то полагаем, что переменная pi оценивается в w в точности так, как произошёл выбор оценки р; при обосновании истинности ір в ходе «разбора» кванториой приставки на г-ом шаге, т. е. если для набора ис-тишюстных значений переменных рі,.. .,Рі_і в мире ги дляр была выбрана «истіша», то мы полагаем, что Pi истинна в w и во всех мирах, достижимых из w , а если значением pt была выбрана «ложь», то полагаем, что pi ложна в w и во всех мирах, достижимых из w \ во всех остальных случаях каждой переменной в каждом мире приписывается оценка «ложь». Ясно, что при таким образом определяемой оценке в міфах уровня п сформировались в точности те наборы истинностных значений переменных pi,... , р„, которые были образованы при обосновании истинности tp (т. е. при которых истинна формула р ), а потому во всех мирах уровня п (т.е. в «самых верхних» міфах) окажется истинной формула р . Поскольку во всех других мирах модели ложна переменная qn, то формула +(qn 4n+i - ) истинна в корне. Проверка истинности в корне всех остальных конъюнктивных членов формулы ір не составляет труда: по сути, даппое выше словесное описание определения оценки есть прочтение этих конъюнктивных членов. Таким образом, р истинна в построенной К4-модели.
Если истинна в некотором мире некоторой К4-модели, то конъюнктивные члены р позволяют «шаг за шагом» выделить подмодель, являющуюся деревом, сходным с тем, которое строилось выше (разве что некоторые миры могут оказаться иррефлексивными), в міфах уровня п которого истинна формула ір , а наборы значений переменных ру,... ,рп в мирах уровня п составляют достаточно представительную выборку для обоснования истинности .
Заметим, что модель, возникающая при обосновании леммы 2.3, может состоять не из рефлексивных, а из иррефлексивных миров или даже как из рефлексивных, так и из иррефлексивных т. е. важна лишь транзитивность отношения достижимости в соответствующей модели. Используя это наблюдение, получаем следующий факт.
Сложность проблемы разрешения позитивного фрагмента: вспомогательная конструкция
Как и выше, для того, чтобы доказать PSPACE-трудность проблемы разрешения Int(2), мы погрузим в Int(2) некоторый фрагмент Int, который обладает PSPACE-полной проблемой разрешения. В качестве такого фрагмента мы возьмём Int — позитивный фрагмент шітуициоїшстской логики. Тот факт, что проблема разрешения для Int+ PSPACE-noraia, следует из [20] (см. также [5] и [43]): при обосновании PSPACE-трудности проблемы разрешения для Int в [20] использовались формулы, построенные из переменных с помощью только конъюнкции и импликации. Заметим, что для обоснования PSPACE-трудности проблемы разрешения логики Int можно использовать те же рассуждения (и те же формулы), что и для случая логик из интервала [BPL,FPL].
Нетрудно видеть, что существует ко такое, что для всякого к ко имеет место отношение 5fc / Nk (действительно, если при подсчёте длины формулы ухватывать только те символы, которые мы используем с учётом сокращений для зашіси отрицашія и договорённости относительно скобок, то І = ІЛдІ + \В1 = 154; тогда начало последовательности чисел віща Ък I выглядит как 154,770,3850,19250,96250,481250,2406250,..., а начало последовательности чисел Nk — как 2,3,4,9,64,3969,15745024,..., и в качестве ко можно взять число 6 или любое большее); для определённости будем считать, что ко — наименьшее число с указанным свойством, т. е. ко — 6.
Теперь построим модель, в которой будут опровергаться все определённые выше формулы, при этом для каждой формулы будет существовать единственный максимальный мир, в котором она опровергается. Поскольку (9Я,а?)[=1 2 и (ЯЯ,а5) = Di V 3, то (ЯЯ.а?) Л?, а следовательно, для всякого мира ад такого, что wRa, имеет место отношение (ЯЯ, ад) \ J4J. Пусть теперь для некоторого мира w Є W выполнено отноше-ние (ЯЯ,ад) Y= А\. Тогда существует мир ад , достижимый из го, такой, что (ЯЯ, го ) f= 2 и (ЯЯ, го ) У=- D\ V D3- Но тогда из ад должны быть достижимы миры d\ и (із и должен быть недостижим міф d2. Заметим, что ад не может быть миром уровня 1 или выше, поскольку из всякого такого мира достижим мир d2\ но среди оставшихся миров модели ЯЯ указанными свойствами обладает только мир а _. Следовательно, w = 0,, и значит, wRa\.
Поскольку {Ж,а%)\=П3 и (9Я,о) i VD2, то (2И,а) [Л, а следовательно, для всякого мира ад такого, что wRa, имеет место отношение (ЯЯ, ад) \ А. Пусть теперь для некоторого мира ад Є W выполнено отноше-шіе (ЯЯ,ад) Л . Тогда существует мир ад , достижимый из ад, такой, что (ЯЯ, ад ) = D2 и (ЯЯ, ад ) Dt V D2. Но тогда из ад должны быть достижимы миры di и d2 и должен быть недостижим мир d3. Заметим, что ад не может быть миром уровня 1 или выше, поскольку из всякого такого мира достижим мир с?2 н0 среди оставшихся миров модели ЯН указанными свойствами обладает только міф а. Следовательно, ад — а[ , и значит, wRa2. Прежде чем начать рассмотрение вопроса о сложности проблемы разрешения фрагментов вида L(n), где L — суперинтуиционистская логика, проведём небольшой анализ уже полученных результатов.
Выше было показано, что логика К4(0) и её «суперинтуиционистский» фрагмент BPL(O) обладают PSPACE-полной проблемой разрешения (см. теоремы 2.9 и 2.28), логика GL(1) и её «суперинтуиционистский» фрагмент FPL(l) тоже обладают PSPACE-полной проблемой разрешения (см. следствие 2.21 и теорему 2.31), причём и GL(0), и FPL(O) полиномиально разрешимы. Может возникнуть гипотеза, что сложность проблемы разрешения «суперинтушшонистского» фрагмента модальной логики Ь{п) всегда совпадает со сложностью проблемы разрешения самой логики L(n). Но, видимо, это не так.
Так, минимальная суперинтуиционистская логика Int является суперинтуиционистским фрагментом всякой модальной логики e[S4, Grz], в частности, Int(n) является суперинтуипионистским фрагментом L(n). В силу следствия 2.17 проблема разрешения для L(l), где L Є [S4, Grz], является PSPACE-трудной. С другой стороны, из конструкции [15] следует, что проблема разрешения для Int(l) находится в классе Р. Таким образом, если бы суперинтуиционистский фрагмент логики 34(1), т.е. логика Int(l), обладал PSPACE-трудной проблемой разрешения, то мы получили бы равенство Р = PSPACE.
Ввиду сомнительности этого равенства навряд ли следует ожидать, что кому-то удастся доказать PSPACE-полноту проблемы разрешения для Int(l); принимая же во внимание определеїшьіе трудности с установлением или опровержением равенства Р = PSPACE, а также тот факт, что сложность проблемы разрешения для Int(l) уже установлена, мы будем рассматривать вопрос о сложности Int(n) для п 2; то же касается и расширений интуиционистской логики, поскольку со многими из них ситуация аналогична только что описанной для Int.
То, что мы заметили, означает, в частности, что нам навряд ли удастся перенести конструкцию, описанную для S4, столь же легко на случай Int (и расширепий Int), как это удалось сделать в случаях с логиками К4 и BPL, а также GL и FPL. Более того, из-за явного отличия ситуации с Int от ситуаций с BPL и FPL можно было бы предполагать, что со сложностью проблемы разрешения Int(n) при п 2 дело обстоит иначе, чем со сложностью разрешения рассмотренных выше фрагментов вида L(n). Например, можно было бы ожидать, что Int(n) полиномиально разрешима для всякого п. Но, тем не менее, как будет доказано ниже, это не так (в предположении, что P PSPACE): уже Int(2) обладает PSPACE-полной проблемой разрешения.
К истокам задачи
Вернёмся к вопросам А.В.Кузнецова [32], о которых говорилось во введении. Напомним их. Первый из них следующий (см. проблему 8 в [32]): является ли Int полиномиально сводимой к С1? Этот вопрос, конечно, равносилен вопросу о полиномиальной эквивалентности Int и С1, поскольку С1 полиномиально сводима к Int в силу теоремы Гливенко, см. [9]. Он останется актуальным, если заменить в нём Int на любую из логик BPL, FPL, К, Т, К4, S4, GL, Grz и др., поэтому мы будем смотреть на этот вопрос шире, считая далее, что логика Int взята лишь для примера. Второй (см. проблему 9 в [32]) формулируется так: является ли логика Int полиномиально финитно аппроксимируемой?
Обратим внимание вот на какой момент. При обосновашш PSPACE-трудности или PSPACE-полноты проблемы разрешения для некоторой логики L мы, вообще говоря, не пытаемся решить проблему равенства классов NP и PSPACE или ответить на вопрос А.В.Кузнецова о полігаомиальноп эквивалентности L и С1. С функцией сложности ситуация иная: оценивая функцию сложности, мы пытаемся получить ответ на второй из упомянутых выше вопросов А. В.Кузнецова, и в случае положительного ответа на него мы получили бы как положительный ответ на первый вопрос, так и положительный ответ на вопрос о равенстве классов NP и PSPACE.
В конце 70-х годов XX века М. В. Захарьящев доказал для большого класса логик (включая как Int, так и другие рассмотренные в данной диссертации логики), что функция сложности для них экспоненциальна (см. [5] и [31]). Таким образом, в случае полного языка ответ на второй вопрос А. В. Кузнецова отрицателен. Первый вопрос при этом остаётся открытым, и результат М. В. Захарьящева лишний раз подчёркивает нетривиальность поставленной А.В.Кузнецовым проблемы.
Поскольку равенство классов NP и PSPACE представляется сомнительным, разумно ожидать, что ответ на первый вопрос также отрицателен. Но вполне разумно рассмотреть близкий вопрос: верно ли, что проблема (р Є Int(n)?» полиномиально сводима к проблеме «ір Є Cl(n)?» (или к проблеме «.(р Є Cl(fc)?» для некоторого к Є N или к проблеме «ірЄ С1? )? Из [15] следует, что это так для Int(O) и Int(l) (аналогичый факт, конечно, справ-ледлив для КС(0), КС(1), S4(0), Grz(O), GL(0) и др.).
К сожалению, диссертант не может дать ответ на вопрос о полиномиальной сводимости Int(2) (и соответствующих фрагментов других рассмотренных в диссертации логик) к Cl(fc) или к CL (а тем самым, ответ на вопрос о равенстве классов Р, NP и PSPACE), но описанная в главе 2 конструкция позволяет получить оценку функщш сложности для соответствующих фрагментов логик.
Заметим, что в случае модальных логик, о которых говорится в теореме 2.1, выполняется следующее: если в качестве булевой формулы с кванторами р брать последовательно формулы вида Vpi... Vpn Т, то при росте п число миров минимальной шкалы Кринке, в которой опровергается формула -нра (в соответствующей модификации, см. раздел 2.2) или формула [tr(ip")]a, будет расти экспоненциально. Это обеспечивается устройством формулы tp : если = Урі.. .Vp„ Т, то истинность формулы tp в корне транзитивной модели гарантирует, что для любого набора истинностных значс-ний переменных pi,..,, р„ в этой модели имеется мир, в котором истинность переменных pi,... ,р„ определена в соответствии с этим набором. Поскольку различных наборов истинностных значений для pi,... ,р„ имеется ровно 2П, то в этой модели должно быть не менее чем 2" миров. Несложно понять, что при переходе от ip к (р ситуация принципиально не изменится: в соответствующей модели должно быть как минимум 2п миров, чтобы учесть все возможные варианты истинности в мире формул ai,..., ап.
Учитывая, что в каждой модификации длина формулы /э (а также длина формулы [fr( )]Q в случае модальных логик) ограничена полиномом от длины формулы р, получаем следующее утверждение.
Обратим внимание на то, что имелось довольно много аргументов ожидать, что фрагменты от конечного числа переменных логик с PSPACE-полной проблемой разрешения в полном языке окажутся полиномиально разрешимы (см. введение). В действительности же ситуация оказалась совсем иной: все рассмотренные нами иеклассические логики, обладающие PSPACE-трудной проблемой разрешения в полном языке, таковы, что для обоснования PSPACE-трудиости этой проблемы достаточно некоторого конечного числа переменных. При этом PSPACE-трудность «канонической» PSPACE-полной проблемы — проблемы выполнимости булевых формул с кванторами — пропадает при переходе к языку с конечным числом переменных (в предположении, что Р ф PSPACE). Возникает естественный вопрос: существует ли неклассическая (суперинтуиционистская, модальная) логика с PSPACE-полной или PSPACE-трудной проблемой разрешения в полном языке, для которой проблема разрешения в языке с п переменными находится в классе Р для любого п?
Отметим, что если ставить аналогичный вопрос с заменой PSPACE на NP, то ответ на него положительный: достаточно рассмотреть логику Кфр«-»Пр. Эта логика погружается в С1 «стиранием» модальностей, откуда следует требуемое.
Сформулированный вопрос далеко не праздный: несложно понять, что если такой логики не существует (хотя бы в классе нормальных модальных логик), то NP PSPACE. Действительно, пусть такой логики не существует. Предположив, что NP = PSPACE, сразу же получаем, что такая логика существует — например, КфрнПр. Полученное противоречие даёт требуемое.
