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

• Пахомов, Федор Николаевич
• кандидат наук
• 2015

Оглавление диссертации кандидат наук Пахомов, Федор Николаевич

Оглавление

Введение

1 Алгоритмическая сложность замкнутых фрагментов

1.1 Логика СЬР и ее замкнутый фрагмент

1.2 Замкнутые фрагменты логик СЬРП

2 Элементарные теории полурешеток СЬР-слов

2.1 СЬР-слова

2.2 Некоторые свойства полурешеток слов

2.3 Определимые в полурешетках слов свойства

2.4 Неразрешимые теории

2.5 Слова из двух символов

3 Элементарные теории системы ординальных обозначений Беклемишева и ее фрагментов

3.1 Системы ординальных обозначений с неразрешимыми элементарными теориями

3.2 Некоторые теории ординалов и слов

3.3 Элементарная эквивалентность некоторых моделей

Литература

Введение диссертации (часть автореферата) на тему «Некоторые алгоритмические вопросы для полимодальных логик доказуемости»

Введение

Диссертация посвящена изучению понятия доказуемости средствами модальной логики. В диссертации исследуются алгоритмические свойства полимодальной логики доказуемости Джапаридзе и ее фрагментов.

Идея изучения свойств доказуемости средствами модальных логик восходит к К. Геделю [20]. Гедель предложил интерпретировать связку модальности □ как арифметическую формулу Ргг, выражающую доказуемость в данной формальной теории Т.

Из результатов Геделя и Леба [25] вытекает, что для перечислимых теорий Т, содержащих первопорядковую арифметику Пеано РА, любая теорема модальной логики GL выражает свойство доказуемости в Т, которое можно обосновать средствами самой теории Т. Логика Геделя-Леба GL формализуется в языке исчисления высказываний, обогащенном связкой □, и получается добавлением к аксиомам и правилам вывода исчисления высказываний следующих аксиом и правил вывода:

1. □(<£> -» ф) -» {Uip ->■ Пф);

2. □(□<£ —»•</?)—>■ П<р (аксиома Леба);

3.

Hip

В 1976 году P.M. Соловей [27] доказал теорему об арифметической полноте логики GL. Модальная формула является теоремой логики GL, если и только если она переводится в теорему РА при любой подстановке арифметических предложений вместо пропозициональных переменных и расшифровке □ как Ргра-

С середины 1970-х годов исследованию логики GL и других логик доказуемости было посвящено значительное число работ. В 1986 г.

Г.К. Джапаридзе рассмотрел [2] обобщение GL — логику GLP, в которой вместо одной модальной связки □ используется занумерованное натуральными числами семейство модальных связок [0], [1],..., [п],... Джапаридзе доказал аналог теоремы Соловея об арифметической полноте, в котором связки [п] интерпретируются как доказуемость из аксиом РА с использованием выводов с w-правилами с глубиной вложенности ы-правил, не превосходящей п.

В настоящее время логика GLP активно изучается в связи с ее применениями в ординальном анализе арифметических теорий [7]. Вопрос о характеризации формальных теорий ординалами является одним из центральных вопросов в теории доказательств. Исследования такого рода восходят к Г. Генцену [19], который доказал непротиворечивость РА с помощью трансфинитной индукции до ординала £q. Применение логики GLP основано на использовании замкнутых формул (формул без пропозициональных переменных) для обозначения арифметических теорий и для построения естественной системы ординальных обозначе-

В диссертации рассматриваются два круга алгоритмических вопросов, связанных с замкнутым фрагментом логики СЬР. 1. Алгоритмическая сложность проблемы распознавания выводимо-

2. Разрешимость элементарных теорий алгебр естественных систем ординальных обозначений.

Вопрос об алгоритмической сложности проблемы выводимости для модальных логик изучался P.E. Ладнером [24]. О Н ПОКЭЗЭЛ 5 что многие классические модальные логики, включая S4, К, Т, обладают PSPACE-полными проблемами распознавания выводимости формул. Хотя логика GL не была рассмотрена в этой работе Ладнера, но использованный там метод легко позволяет получить аналогичный результат и для нее. В дальнейшем, И.Б. Шапировский доказал, что и логика GLP

ний для ординала £q = sup{

| п G ш}.

сти.

обладает PSPACE-полной проблемой распознавания выводимости [26].

А.В. Чагровым и М.Н. Рыбаковым рассматривались фрагменты модальных логик с ограничением на число различных пропозициональных переменных в формулах и вопрос об алгоритмической сложности для этих фрагментов [15]. Ими было показано, что даже фрагмент логики GL с одной пропозициональной переменной является PSPACE-полным; там же были получены аналогичные результаты для логик S4 и Grz. При этом они показали, что замкнутый фрагмент логики GL разрешим за полиномиальное время. В то же время замкнутые фрагменты логик К4 и К являются PSPACE-полными. Также Ф. Boy и Й. Йоостен доказали, что замкнутый фрагмент логики интерпретируемости IL, расширяющей GL, является PSPACE-трудным [12].

В диссертации доказана PSPACE-полнота замкнутого фрагмента логики GLP.

Мы обозначаем через GLPn фрагмент логики GLP с модальностями [0], [1],..., [п]. Также доказано, что для всякого натурального п замкнутый фрагмент логики GLPn разрешим за полиномиальное время.

Перейдем к вопросам разрешимости элементарных теорий алгебр, связанных с конструктивными системами ординальных обозначений. Наиболее известной системой обозначений для ординала £q является так называемая канторовская система. Обозначениями для ординалов в этой системе являются замкнутые термы, составленные из константы 0, функции + и функции /: х \—у их. Канторовская система соответствует алгебре (ео; <, 0, +, /); заметим, что в этой алгебре всякий ординал меньший £q равен значению некоторого замкнутого терма. Известно, что элементарная теория модели (его; <, 0, +, /) является алгоритмически неразрешимой.

Естественный, связанный с ординальным анализом способ обозначения ординалов на основе замкнутого фрагмента логики GLP был предложен Л.Д. Беклемишевым [7]. Ординалы обозначаются формула-

ми вида (ni) (ni)... (пк)Т, называемыми словами. Мы обозначаем множество всех слов W. Бинарное отношение <о на словах соответствует порядку на ординалах:

А<0В GLP h А —>• (0)В.

Отношение равенства ординалов соответствует отношению GLP-доказуемой эквивалентности слов Полной системе орди-

нальных обозначений для ординала £о соответствует алгебра ( W/~\ <о, Т, (0), (1),..., (п),...). Также мы рассматриваем ряд естественных фрагментов этой системы ординальных обозначений. Обозначим через Wn множество всех слов составленных из Т и (0 ),..., (п); мы называем такие слова СЬРп-словами. Модель ( <0; Т, (0), (1),..., (п)) является системой ординальных обозна-

чений для ординалов ип+1; здесь

uj0 = 1, ujn+x = иШп.

Отметим, что конъюнкция всяких двух слов GLP-доказуемо эквивалентна некоторому GLP-слову [7]. Это дает возможность естественным образом рассматривать полурешетки (W/~;A) и (Wn/~; А).

Е.В. Дашков [1] рассмотрел фрагмент логики GLP, состоящий из импликаций между строго позитивными формулами, то есть между формулами построенными из переменных, А, Т и (0), (1),... (п). Он показал, что проблема выводимости формул для этого фрагмента лежит в классе PTIME, в противоположность тому, что логика GLP и даже ее замкнутый фрагмент PSPACE-полны. Отметим, что из результата Е.В. Дашкова следует разрешимость за полиномиальное время диаграмм моделей {W/~\ А, <о, Т, (0), (1),..., (п),...) и ( А, <о, Т, (0), (1),..., (п)).

В диссертации доказано, что элементарная теория модели ( <о, Т, (0), (1),..., (п),...) неразрешима. Доказано, что при всех п > 3 неразрешимы элементарные теории моделей

(<о> Т, (0), (1),..., (п)). При этом показано, что элементарная теория модели (<о> "Г, (0), (1), (2)) разрешима. Доказано, что языка первого порядка в полурешетках и (МКП/~;Л)

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

Методы исследования. В работе используются методы теории сложности вычислений, модальной логики и теории моделей. Для доказательства РБРАСЕ-полноты замкнутого фрагмента логики СЬР строится полиномиальное сведение языка булевых формул с кванторами к искомому. Полиномиальные разрешающие алгоритмы для замкнутых фрагментов СЬРП основаны на эффективном кодировании подмножеств предложенной К.Н. Игнатьевым [22] универсальной модели Крип-ке для замкнутого фрагмента логики СЬР. Мы доказываем неразрешимость элементарных теорий полу решеток СЬР-слов, интерпретируя в них неразрешимую [18] слабую монадическую теорию натуральных чисел в сигнатуре, включающей в себя функцию следования и функцию Н(х) = 2х. Для доказательства разрешимости элементарной теории полу решетки строится ее интерпретация в теории структуры <,+). Результаты о неразрешимости элементарных теорий системы ординальных обозначений Беклемишева и ее фрагментов доказываются путем погружения теории класса всех пар линейных порядков на конечных множествах. Разрешимость теории элементарной теории модели (Ж2/~; <о, Т, (0), (1), (2)) доказывается при помощи построения ее интерпретации в слабой монадической теории ординаласнабженного порядком и предикатом задающим стандартную систему кофинальных последовательностей, разрешимость которой была установлена Л. Бро [13].

Содержание работы

Глава 1 содержит доказательство РБ РАС Е-пол ноты проблемы распознавания выводимости для замкнутого фрагмента логики СЬР и доказательства полиномиальной разрешимости проблем распознавания выводимости для замкнутых фрагментов логик СЬРП.

Основной результат главы 2 состоит в доказательстве неразрешимости элементарной теории полурешетки СЬР-слов. Кроме того, установлено, что элементарная теория полурешетки СЬРп-слов неразрешима, если и только если п> 2.

Глава 3 посвящена исследованию элементарных теорий систем ординальных обозначений на основе логики СЬР. Доказано, что алгебра соответствующая полной системе ординальных обозначений для ординала £о обладает неразрешимой элементарной теорией. Также в главе 3 доказывается, что элементарная теория алгебры, соответствующей системе ординальных обозначений, порождаемой (0),..., (п), неразрешима при п > 3 и разрешима при п = 2.

Язык полимодальной логики доказуемости СЬР — это язык исчисления высказываний с пропозициональными константами «истина» Т и «ложь» _1_, обогащенный унарными связками [0], [1],.... Запись {п)(р является сокращением для —>[п]~ир. СЬР задается следующими аксиомами и правилами вывода:

0. Аксиомы и правила вывода логики СЬ для каждой связки [гг];

1. [к](р —у [п]1р, где к < щ

2. (к)ср —> [п](к)(р, где к < п.

Мы обозначаем через СЬРП логику, язык которой получается из языка пропозициональной логики обогащением связками [0],..., [п], а теоремами являются все теоремы СЬР в этом языке.

В главе 1 доказывается

Теорема 1. Проблема распознавания выводимости замкнутых формул в логике СЬР является РБРАСЕ-полной.

Далее в этой главе доказывается, что наличие бесконечного числа различных модальных связок в языке необходимо для получения РБ РАС Е-по л ноты.

Теорема 2. При всех п проблема распознавания выводимости замкнутых формул в логике СЬРП разрешима за полиномиальное время.

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

Одним из центральным для глав 2 и 3 понятием является понятие СЬР-слова. Рассматривается множество \¥ всех формул вида (п1)(п2)... (пк)Т. Такие формулы называются СЬР-словами также для краткости в рамках данной диссертации мы называем их просто словами. Для обозначения слов мы используем буквы А, В,....

На множестве всех СЬР-формул определим бинарные отношения

(р <пф СЬР Ь ф (п)<р.

Мы обозначаем через ~ отношение СЬР-доказуемой эквивалентности на формулах и, в частности, на словах:

ср ~

ф СЬРЬср^ф.

Как было отмечено выше, конъюнкция двух слов в СЬР эквивалентна некоторому слову. Тем самым, связки (п) и А естественным образом задают функции на классах эквивалентности слов:

<га>[А]_ = {В | В - <п)А}, [А]„ А [В]„ = {С | С - А А В}.

В главах 2 и 3 мы изучаем разрешимость элементарных теорий моделей Л, <о,Т, (0), (1), ...,(&),...), (Л, <о, Т, (0), (1),..., (п)) и моделей, получаемых из них опусканием некоторых предикатов и функций. Отметим, что фактически из соображений технического удобства мы работаем не непосредственно с этими моделями, а с изоморфными моделями, носители которых составлены из слов в нормальной форме (канонических представителей классов эквивалентности СЬР-слов по отношению

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

Теорема 3. Элементарная теория нижней полурешетки (Ж/^Л) неразрешима. При всех п > 2 неразрешимы элементарные теории полурешеток (ИУ~;Л).

Отметим, что при доказательстве этой теоремы мы устанавливаем, что в (Л) формулами первого порядка выразимы все бинарные отношения <к и все функции (к). Более того мы доказываем, что для всех натуральных п в (Л) формулами первого порядка выразимы все бинарные отношения <к и все функции (к) при к < п.

Теорема 4. Элементарная теория нижней полурешетки разрешима.

В главе 3 мы изучаем вопрос об разрешимости элементарных теорий моделей с носителями ~ или ]¥п/~ и сигнатуре могущей включать лишь предикат <о, константу Т и функции (к). Отметим, что модель (Ш~:<о;Т,(0),<1),...,(А;),...) и <0, (0), (1),..., <п» являются естественными конструктивными представлениями ординалов £о и соответственно.

Теорема 5. Пусть р, # и п — натуральные числа такие, что 0 < р и р + 1 < д < п. Тогда элементарные теории моделей <о, (р), (<?))

и (<0, (р), (д)) неразрешимы.

Модель <о> Т, (0), (1),..., (к),...), в силу теоремы 5, име-

ет неразрешимую элементарную теорию. Также, из этой теоремы следует, что при всех п > 3 неразрешима элементарная теория модели (<0, Т, (0), (1),..., {п)).

Кроме того мы устанавливаем следущие теоремы.

Теорема 6. Для модели <о,Т, (0), (1), (2)) элементарная тео-

рия разрешима при всех п > 2.

Теорема 7. Элементарная теория модели (<о, Т, (0), (1), (2)) разрешима. При всех п > 2 элементарная теория модели (И/п/~; <0) Т, (0), (1), (2)) разрешима.

Для доказательства теоремы 7 мы показываем, что все структуры (И/п/~; <о, Т, (0), (1), (2)), где п > 3, и структура (<о, Т, (0), (1), (2)) попарно элементарно эквививаленты, а далее применяем теорему 6.

Я выражаю глубокую благодарность своему научному руководителю члену-корреспонденту РАН Л.Д. Беклемишеву за постановку задач и поддержку в работе. Я благодарю участников семинаров «Логические проблемы информатики» и «Алгоритмические проблемы алгебры и логики» за конструктивное обсуждение. Кроме того, я благодарю за полезные замечания анонимных рецензентов своих статей по теме диссертации.

Глава 1

Алгоритмическая сложность замкнутых фрагментов

1.1 Логика СЬР и ее замкнутый фрагмент Логика СЬР.

Совокупность всех правильно построенных СЬР-формул порождается пропозициональными переменными х\, ..., хп,..., двуместными пропозициональными связками А, V, —>-, одноместной пропозициональной связкой -1, пропозициональными константами Т (истина), _1_ (ложь) и унарными модальными связками [0], [1],..., [и],... Мы вводим связки (п) следующим образом:

{п)(р ^ -1[п]

Логика СЬР задается следующими схемами аксиом и правилами вывода:

1. Схемы аксиом исчисления высказываний в расширенном языке;

2. [п](</> ^ф)^ ([п]</> ->- [п]ф)\

3. [п]([п]</7 ф) ->• [п)(р\

4. [к](р —» [п]<£>, где к< щ

5. (к)<р —)■ [п](к)(р, где к < щ ш (р^-ф

6---;

ф

[п]р

Мы называем GLP-формулу замкнутой, если в ней не содержатся пропозициональные переменные.

В этом разделе мы доказываем следующую теорему.

Теорема 1. Проблема распознавания выводимости в логике GLP для замкнутых формул является PSPACE-полной.

Из теоремы Шапировского [26] о PSPACE-полноте проблемы распознавания выводимости в логике GLP следует принадлежность проблемы из теоремы 1 к классу PSPACE. В силу этого, для доказательства теоремы 1 достаточно показать, что проблема является PSPACE-трудной.

Обозначим через QBF проблему распознавания истинности булевых формул с кванторами. Известно, что QBF является PSPACE-полной [28]. Для доказательства PS РАСЕ-сложности проблемы распознавания выводимости в GLP замкнутых формул мы строим полиномиальную редукцию проблемы QBF к данной. Пусть имеются формулы

QqXOQIXI ... Q n— 1 ) 1 ) ,

где Qj G {V, 3}, a <p(xq, ..., xn-i) — булева формула, переменныеч входящие в которую исчерпываются набором xq, ..., £n-i- Мы построим полимодальные формулы щ и фо такие, что булева формула с кванторами

QQXqQIXI ... Q

п—1%п—

истинна, если и только если

GLP h туе о ф0-

Отметим, что в языке GLP нет связки -В-, и мы выражаем ее с помощью связок Л и —Кратко опишем идею построения формулы 1. Мы начинаем со специально подобранных, полностью логически независимых формул во,..., 0п_ т.е. таких формул, что для всякой формулы ... ; хп-\) языка исчисления высказываний £ является тавтологей если и только если GLP h • • •, On-i/zo, ■ ■ ■, хп-1]■

2. Далее мы рассматриваем формулу

фп ^ р[0о, • • •, Оп-г/хо,..., Хп-г].

Отметим, что если бы нашей проблемой было сведение проблемы распознавания доказуемости формул в исчислении высказываний к проблеме распознавания доказуемости замкнутых формул в логике СЬР, то проделанного было бы достаточно.

3. Наша цель состоит в построении формул фо,..., фп-\- Для каждого г от 1 до и формула ф^ в некотором смысле, представляет формулу

... Оп_1Хп_1(/?(жо,..., жг_1, Х{,..., хп-.\) жг_1 замененными

на во,..., 0г-_1 соответственно.

4. Мы получаем формулу ф{ как £[ф{+г/х], где £ это некоторая короткая формула. Конкретный вид £ зависит от того, каким именно квантором является С^, а также чисел п и i. Кроме того, х является единственной переменной в при этом х встречается в £ ровно один раз и при этом позитивно.

5. Оказывается, что имеет место ровно одна из двух альтернатив:

(a) формула фо является СЬР-опровержимой (т.е. ОЬР I—>фо) и

(ЗоаьСЬж!... (¿п-гхп-^хо,..., ж^)

ложна,

(b) формула фо оказывается вЬР-доказуемо эквивалентной специальной формуле щ и

ОоЯоСЬя!... Ъ^Хп-цр^о, ■ • •, жп_х)

истинна.

Мы определяем следующие формулы

1. г}п ^ Т;

2. гц ^ (2г)(4п - 2г - 1)Т для 0 < г < щ

3. вг ^ (2г + 1)(4п — 2г — 2)Т для 0 < г < щ

4. фп ^ (/>[00, • • •, 6п-i/жо,. . . , Хп-г]\

5. ipi ^ (2г)(4п — 2г — 1)(2г)^+1 для 0 < г < п, в случае Q* = 3.

6. r)i Л -|(2г)(4га — 2 г — 1}(2г)(т7»+1 А —>-0t-+i) для 0 < г < п, в случае Q= V.

Для ВСЯКОЙ формулы £ ПОЛОЖИМ £Т ^ £ И £J- ^ Для каждого 0 < к < п обозначим через Ак множество всех функций а: {0,..., к — 1} —> {-L, Т} таких, что истинна булева формула с кванторами

Qkxk... Qn_ixn_i(p(a(0), ...,а(к- 1),хк,...,

Через Л^ мы обозначим дополнение Л* до множества всех функций а: {0,..., к — 1} —> {_L,T}. Отметим, что существует единственная функция а: 0 —> {_L,T}, а следовательно |Ло| = 1, если Qo^b • • • Q„-iaVi-iy(ai), • ■ ч xn-i) истинна и |Л0| = 0, иначе.

Лемма 1.1. [8, лемма 1] Пусть £2 являются полимодальными формулами и si, 52 натуральными числами такими, что si < 52. Тогда

1. glp н (52) (а л <sl)£2) ^ (¡bki л ыа-

2. glp ь <в2>й1 л ыб a

Следующая лемма может быть легко получена из следствия 2.7, которое будет доказано позднее:

Лемма 1.2. Пусть s — натуральное число и формула </? имеет вид (si) ... (sn)T, где Sj < s для всех i. Тогда

GLP h (s)<p (s)T. Замечание 1.3. Дизъюнкцию пустого множества формул \J £ мы считаем равной J_. Конъюнкцию пустого множества формул Д £ мы считаем равной Т. Лемма 1.4. Пусть к < п. Тогда

glpb у (т а^ фк.

ае Ак i<k

Доказательство. Мы доказываем лемму индукцией по п — к. Формула V ( Л является совершенной дизъюнктивной нормальной формой

сгбЛ„ i<n

для (р. Следовательно предположение индукции имеет место для случая к = п. Далее мы доказываем переход индукции.

Рассмотрим случай Qk = 3. Мы даем последовательность замкнутых формул языка логики GLP и затем показываем, что соседние формулы в этой последовательности GLP-доказуемо эквивалентны:

1- Фк;

2. (2к)(Ап-2к-1)(2к)фк+ъ

3. (2к)(Ап-2к-1)(2к)( V ЫiA Л 0?(0));

aeAk+i i<k+1

4. V (2к)(4п-2к-1)(2к)(г1к+1Л Д ef]y,

<7eAfc+i i<k+l

5. V ((2fc)(4n - 2k — l)(2k)(rjk+i A 0™) Л Д

crGAfc+i i<k

6. V ((2fc)(4n — 2k— 1)T А Д ;

«тел*;

Очевидно, что пары (l.,2.), (2.,3.), (3.,4.) и (6.,7.) являются парами GLP-доказуемо эквивалентных формул. Эквивалентность 4. и 5. может быть обоснована с помощью многократного применения леммы 1.1. Для установления GLP-доказуемой эквивалентности 5. и 6. мы докажем, что

GLP h (4п —2к— l)(2k)(rik+i Л вк) (4п - 2к - 1>Т, (1.1)

GLP h {4п-2к-1)(2к)(г]к+1 Л^вк) (4п — 2к— 1)Т. (1.2) Из леммы 1.1 следует, что

GLP h щ+1 Л 0к (2к + 2)(4п — 2к—3)(2к + 1)(4п -2к- 2)Т.

В силу леммы 1.2

GLP h (4п — 2к — 1) (2к) (2к + 2) (4п -2к-3) (2к + 1) (4п - 2к - 2)Т ++

(4тг — 2к— 1)Т.

Поэтому эквивалентность (1.1) выполняется.

Докажем, что GLP I—1(2k)r)k+i —>

GLPh вк^ (2к)(4п-2к-2)Т

-> (2к)(Ап — 2к— 2) (4га — 2к— 3)Т (2к)(2к+ 2) (4га — 2к— 3)Т

Используя аксиому 3 логики GLP, мы выводим

GLP h (2к)щ+1 (2й)(%+1 Л -.(2

(2Л>(т7ан-1 A^jfc).

Поэтому мы имеем

GLP h (4га -2к-1) (2к)щ+1 (4га - 2к - 1) (2fc) (77^+1 Л -.0*). Следовательно, в силу леммы 1.2 мы имеем

GLP h (4га - 2к - 1)Т (4га -2к-1) (2к)г)Ш

{4п - 2к - 1}(2к){т]к+1 А

Следовательно, эквивалентность (1.2) имеет место.

Таким образом, формулы 5. и 6. являются GLP-доказуемо эквивалентными. В результате мы получаем, что формулы 1. и 7. эквивалентны в GLP. Это завершает обоснование перехода индукции в случае Qk = 3.

Перейдем к случаю Qk = V. Мы рассматриваем следующую последовательность замкнутых GLP-формул:

1- Фк]

2. щ А -(2£)(4га -2к- l)(2k)(r]k+1 А ^<фк+

3. r)k А ->(2&)(4га — 2к— 1){2к){щ+\ А ->( V Л Д в^)));

aeAk+i Кк+1

4. rjk Л -i(2fc)(4n — 2к— 1)(2к)( V А Д С^)); 5- V (^ЛД0Г(г)));

е. У(%лД0Г(г)).

<7GAfc г< А:

Для всех пар соседних формул, кроме 4. и 5. очевидно, что эквивалентность имеет место. Последняя эквивалентность обосновывается аналогично эквивалентности между 3. и 7. из доказательства перехода индукции в случае Q^ = 3. □

По лемме 1.4, мы имеем GLP Ь щ -в- если формула

истинна, и GLP Ь JL ^О) если формула ложна. Из корректности арифметической семантики [22] для логики GLP легко выводится, что GLP I/ ?7о -н- _L (также этот факт легко доказать с помощью модели Игнатьева, чье описание мы приводим в следующем разделе). Следовательно

Qo^Qi^i... Q

п— 1

Х(р(хо, ■ . . , Xn-i)

истинна тогда и только тогда, когда

GLP h 77о ^ ф0.

Несложная проверка показывает, что мы можем получить формулу г}о -н- фо за полиномиальное время от длины

QqXqQiXi . . . Qn-l^n-l^^O, Xi, ..., xn-i). Это дает нам требуемое сведение и завершает доказательство теоремы 1.

1.2 Замкнутые фрагменты логик GLPn

Правильно построенные формулы логики GLPn — это GLP-формулы, в которых из модальных связок встречаются только [0], [1],..., [п]. Исчисление в гильбертовском стиле для логики GLPn задается теми аксиомами и правилами вывода исчисления для GLP, которые лежат в языке логики GLPn. Отметим, что множество теорем логики GLPn совпадает со множеством теорем логики GLP, которые являются СЬРп-формулами [10].

Метод использованный в предыдущем разделе существенно использует бесконечно много модальностей и, тем самым этот метод не может быть использован для доказательства РБ РАСЕ-трудности проблемы распознавания выводимости замкнутых формул в логиках СЬР„.

Центральным результатом этого раздела является следующая теорема.

Теорема 2. При всех натуральных п проблема распознавания выводимости в логике СЬРП для замкнутых формул разрешима за полиномиальное время.

Начнём с плана доказательства. Мы используем модель Крипке (определение понятия модели Крипке см. [11 ])Ы£ такую, что замкнутый фрагмент логики СЬРП является полным относительно этой модели. Каждой замкнутой СЬРп-формуле мы ставим в соответствие множество миров модели , в которых она выполняется. Полнота замкнутого фрагмента СЬРП относительно модели означает, что всякая за-

мкнутая СЬРп-формула доказуема в СЬРП тогда и только тогда, когда этой формуле соответствует множество всех миров модели . Отметим, что для всякой замкнутой СЬРп-формулы <р> соответствующее ей множество может быть получено интерпретацией пропозициональных констант и пропозициональных связок из (р, как специальных множеств миров и специальных операций на множествах миров , соответственно.

Мы используем коды из множества для эффективного представления множеств миров модели (отметим, что существуют множества миров, которым не соответствует ни одного кода). В разрешающем алгоритме мы используем следующие вычислимые функции (в полном доказательстве у них имеются дополнительные аргументы и параметры) :

1. 1Шг: С

2. Стр1: С

3. С£п+1->С£п+1,

4. 1зЕтр: С£п+1{0,1}.

Наш разрешающий алгоритм работает таким образом:

1. Мы получаем на вход замкнутую СЬРп-формулу (р.

2. Мы заменяем ее на формулу (рг такую, что

вЬР \~<р'<гкр

и (р' составлена из _1_, А, [0],..., [п].

3. Мы строим код с(<£>') для множества, соответствующего формуле (р'. Для этого мы определяем коды с(ф) для всех подформул ф формулы (р', используя следующие правила:

(a) с(_1_) является константой, обозначающей пустое множество;

(b) А ф2) равно 1пгг{с{ф\), с{ф2))\

(c) с(->ф) равно Стр1(с(ф))-, (с!) с((к)ф) равно Нк-1пу(с(ф)).

4. Мы даем положительный ответ на формулу (р, если и только если функция 1зЕтр возвращает 1 на входе Стр1(с (<//))•

Теперь опишем наш метод оценки времени работы алгоритма. Мы вводим функции с"п+1 и для измерения сложности кодов, переданных на вход. Далее мы получаем оценки времени работы и сложности результирующих кодов для функций Стр1, 1пЫ, Яо-1пу, В,1-1пу,. .11п-1пу в терминах сложности кодов на входе. Это дает нам полиномиальную оценку на сложности используемых кодов, в смысле указанных выше функций, и на время работы разрешающего алгоритма. В большинстве лемм этого раздела мы одновременно даем описание алгоритма и верхнюю оценку на время его работы.

Теперь мы переходим к точному описанию требуемой нам модели Крипке.

Обозначим через Оп класс всех ординалов.

Теорема Кантора о нормальной форме ординалов утверждает, что каждый ординал а > 0 может быть единственным образом представлен в виде суммы

а = а/0 Н----+ аА"1

такой, что /Зо > > ... > Рп-1 и п > 0. Пусть 1\ Оп^ Оп задается, как • ¿(0) = 0;

• £(а) — где а > 0 и КНФ (канторовская нормальная форма) а

равна и/0 +----1- и/3"-1.

Определим модель Игнатьева Ы = (С/, По, Яь ..., Яп, • • •) [22]. Множество и является множеством всех последовательностей

(а0,а1,а2,...)

таких, что все аг- являются ординалами, ао < £о и < ^(^г), Для всех г Е у. Для каждого натурального к бинарное отношение 11* задается, как

Оо, аъ ...) Я* (/0О, (Зъ ■■■) ^ рк<акАУг< %« = А)-

Модель Ы является универсальной моделью для замкнутого фрагмента логики вЬР [22, 23, 9]. Это означает, что для всякой замкнутой СЬР-формулы (р мы имеем

вЬР Ь <р -<=>- и [= (р {(р верна в Ы).

Легко видеть, что для всякой последовательности (ско, , • • •) £ и мы имеем = 0 для достаточно больших г.

На самом деле, нам потребуются «меньшие» модели Ы£ = (Щ, Т1о, Яь • • •, Яп) для всевозможных 1<а<£оИ7г> — 1- Отметим, что все и~1 будут моделями исчисления высказываний РС = СЬР_1 с единственным миром и без отношений достижимости. Для а < £о множество и™ С и является множеством всех последовательностей ординалов

Список литературы диссертационного исследования кандидат наук Пахомов, Федор Николаевич, 2015 год

Литература

1] Е.В. Дашков. О позитивном фрагменте полимодальной логики доказуемости GLP. Математические заметки, 91(3):331—346, 2012.

2] Г.К. Джапаридзе. Модально-логические средства исследования доказуемости. Дисс. канд. филос. наук, Москва, МГУ, 1986.

3] Ю.Л. Ершов, И.А. Лавров, А.Д. Тайманов и М.А. Тайцлин. Элементарные теории. Успехи математических наук, 20, 4(124):37—108, 1965.

4] Ю.Л. Ершов. Проблемы разрешимости и конструктивные модели Наука, 1980.

5] И.А. Лавров. Эффективная неотделимость множества тождественно истинных и множества конечно опровержимых формул некоторых теорий. Алгебра и Логика Семинар, 2(1):5—18, 1963.

6] J. Barwise. Admissible Sets and Structures. Perspectives in mathematical logic. Springer, 1975.

7] Lev D. Beklemishev. Provability algebras and proof-theoretic ordinals, I. Annals of Pure and Applied Logic, 128:103-123, 2004.

8] Lev D. Beklemishev. Veblen hierarchy in the context of provability algebras. In Logic, Methodology and Philosophy of Science, Proceedings of the Twelfth International Congresspages 65-78. Kings College Publications, 2005.

[9] Lev D. Beklemishev, Joost J. Joosten, and Marco Vervoort. A finitary treatment of the closed fragment of Japaridze's provability logic. J. Log. Comput., 15(4):447-463, 2005.

[10] Lev D. Beklemishev, David Fernández-Duque, and Joost J. Joosten. On provability logics with linearly ordered modalities. Studia Lógica, 102(3):541-566, 2014.

[11] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic: Graph. Darst. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2002.

[12] Félix Bou and Joost J. Joosten. The closed fragment of IL is PSPACE hard. Electronic Notes in Theoretical Computer Science, 278:47-54, 2011.

[13] Laurent Braud. Covering of ordinals. In FSTTCS, pages 97-108, 2009.

[14] J.R. Biichi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(l-6):66-92, 1960.

[15] Alexander V. Chagrov and Mikhail N. Rybakov. How many variables does one need to prove pspace-hardness of modal logics? In Advances in Modal Logic 4 (AiML'02. Citeseer, 2003.

[16] Stephen A. Cook and Robert A. Reckhow. Time bounded random access machines. J. Comput. Syst. Sci., 7(4):354-375, August 1973.

[17] Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129141, 1961.

[18] C.C. Elgot and M.O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. J. Symb. Log., 31:169-181, 1966.

[19] Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493-565, 1936.

[20] Kurt Godel. Eine Interpretation des intuitionistischen Aussagenkalküls. Ergebnisse eines mathematischen Kolloquiums, 4: 39-40, 1933. English translation, with an introductory note by A.S. Troelstra. Kurt Gódel, Collected Works, 1:296-303, 1986.

[21] W. Hodges. Model Theory. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.

[22] K.N. Ignatiev. On strong provability predicates and the associated modal logics. The Journal of symbolic logic, 58(l):249-290, 1993. eng.

[23] Joost J. Joosten. Interpretability formalized. Ph.D thesis, Utrecht University, 2004.

[24] Richard E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM journal on computing, 6(3):467-480, 1977.

[25] Martin Hugo Lob. Solution of a problem of Leon Henkin. The Journal of Symbolic Logic, 20(02):115-118, 1955.

[26] Ilya Shapirovsky. PSPACE-decidability of Japaridze's polymodal logic. In Advances in Modal Logic, pages 289-304, 2008.

[27] Robert M. Solovay. Provability interpretations of modal logic. Israel journal of mathematics, 25(3-4) :287-304, 1976.

[28] L. J. Stockmeyer and A. R. Meyer. Word problems requiring exponential time(preliminary report). In Proceedings of the Fifth Annual ACM Symposium on Theory of Computing, STOC '73, pages 1-9, New York, NY, USA, 1973. ACM.

[29] A. Tarski and A. Mostowski. Arithmetical classes and types of well ordered systems. Bull. Amer. Math. Soc., 55:65, 1949.

[30] A. Tarski, A. Mostowski, and R.M. Robinson. Undecidable Theories. Studies in logic and the foundations of mathematics. North-Holland, 1953.

Работы автора по теме диссертации

[31] Ф.Н. Пахомов. Неразрешимость элементарной теории полурешетки GLP-слов. Математический сборник, 203(8): 141-160, 2012.

[32] Ф.Н. Пахомов. Об элементарных теориях систем ординальных обозначений на основе схем рефлексии. Труды Математического института им. В.А. Стеклова, 289:206-226, 2015.

[33] Fedor Pakhomov. On the complexity of the closed fragment of Japaridze's provability logic. Archive for Mathematical Logic, 53(7-8):949-967, 2014.