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

ФГБУН Математический институт им. В.А. Стеклова Российской академии наук

На правах рукописи УДК 510.643

Пахомов Федор Николаевич

Некоторые алгоритмические вопросы для полимодальных логик доказуемости

Специальность 01.01.06 — математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

5 АВГ 2015

005571290

Москва 2015

005571290

Работа выполнена в отделе математической логики ФГБУН Математический институт им. В.А. Стеклова РАН

Научный руководитель: Беклемишев Лев Дмитриевич,

член-корр. РАН,

доктор физико-математических наук, главный научный сотрудник отдела математической логики ФГБУН Математический институт им. В.А. Стеклова РАН (специальность 01.01.06).

Официальные оппоненты: Варданян Валерий Арамович,

кандидат физико-математических наук, старший научный сотрудник, советник директора ФГБУН Вычислительный центр им. A.A. Дородницына РАН (специальность 01.01.06);

Шехтман Валентин Борисович, доктор физико-математических наук, главный научный сотрудник сектора 4.1 (Алгебра и теория чисел) ФГБУН Институт проблем передачи информации им. A.A. Харкевича РАН (специальность 01.01.06).

Ведущая организация: ФГБУН Институт математики

им. С. JL Соболева СО РАН.

Защита диссертации состоится 22 октября 2015 года в 14 часов 00 минут на заседании диссертационного совета Д 002.022.03 при МИАН по адресу: РФ, 119991, Москва, ул. Губкина, д. 8, конференц-зал (9 этаж).

С диссертацией можно ознакомиться в библиотеке МИАН по адресу: РФ, 119991, Москва, ул. Губкина, д. 8, 8 этаж, а также на сайте http://www.mi.ras.ru/dis/ref15/pakhomov/pakhomov_dis.pdf.

Автореферат разослан июля 2015 года.

Ученый секретарь диссертационного совета Д 002.022.03 при МИАН, доктор физико-математических наук И.Д. Шкредов

Общая характеристика работы

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

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

Логика Геделя-Леба GL формализуется в языке исчисления высказываний, обогащенном связкой □, и получается добавлением к аксиомам и правилам вывода исчисления высказываний следующих аксиом и правил вывода:

1. D(<p ->■ V) ->■ (Dip Пф)]

2. □(□у? —> <р) —> Dtp (аксиома Леба);

3- FT-Dip

Из результатов К. Геделя и М.Х. Леба2 вытекает, что для перечислимых теорий Т, содержащих первопорядковую арифметику Пеано РА, любая теорема модальной логики GL выражает свойство доказуемости в Т, которое можно обосновать средствами самой теории Т.

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

С середины 1970-х годов исследованию логики GL и других логик доказуемости было посвящено значительное число работ. В 1986 г. Г.К. Джапаридзе рассмотрел4 обобщение GL — логику GLP, в которой вместо одной модальной связки □ используется занумерованное натуральными

1К. Gödel. 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.

2M.H. Löb. Solution of a problem of Leon Henkin. The Journal of Symbolic Logic, 20(02):115-118, 1955.

3R.M. Solovay. Provability interpretations of modal logic. Israel Journal of Mathematics, 25(3-4) :287-304, 1976.

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

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

В настоящее время логика GLP активно изучается в связи с ее применениями в ординальном анализе арифметических теорий5. Вопрос о характеризации формальных теорий ординалами является одним из центральных вопросов в теории доказательств. Исследования такого рода восходят к Г. Генцену6, который доказал непротиворечивость РА с помощью трансфинитной индукции до ординала £о = | п 6 со}.

п раз

Применение логики GLP основано на использовании замкнутых формул (формул без пропозициональных переменных) для обозначения арифметических теорий и для построения естественной системы ординальных обозначений для ординала cq.

В диссертации рассматриваются два круга алгоритмических вопросов, связанных с замкнутым фрагментом логики GLP.

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

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

Вопрос об алгоритмической сложности проблемы выводимости для модальных логик изучался Р.Э. Ладнером7. Он показал, что многие классические модальные логики, включая S4, К, Т, обладают PSPACE-полными проблемами распознавания выводимости формул. Хотя логика GL не была рассмотрена в этой работе Р.Э. Ладнера, использованный там метод легко позволяет получить аналогичный результат и для нее. В дальнейшем, И.Б. Шапировский доказал, что и логика GLP обладает PSPACE-полной проблемой распознавания выводимости8.

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

6G. Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493-565, 1936.

7R.E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing, 6(3):467-480, 1977.

8I.B. Shapirovsky. PSPACE-decidability of Japaridze's polymodal logic. In Advances in Modal Logic 2008, pages 289-304, 2008.

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

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

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

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

Естественный, связанный с ординальным анализом способ обозначения ординалов на основе замкнутого фрагмента логики GLP был предложен Л.Д. Беклемишевым в его указанной выше работе5. Ординалы обозначаются формулами вида (ni) (ni)... называемыми словами. Мы обозначаем множество всех слов W. Бинарное отношение <о на словах соответствует порядку на ординалах:

А<0В GLP Ь А —(0)В.

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

9 A.V. Chagrov and M.N. Rybakov. How many variables does one need to prove PSPACE-hardness of modal logics? In Advances in Modal Logic 2002, pages 71-82. King's College Publications, 2003.

10F. Bou and J.J. Joosten. The closed fragment of IL is PSPACE hard. Electronic Notes in Theoretical Computer Science, 278:47-54, 2011.

нальных обозначений для ординала £о соответствует алгебра ( <о, Т, (0), (1),..., (п),...). Также мы рассматриваем ряд естественных фрагментов этой системы ординальных обозначений. Обозначим через Wn множество всех слов составленных из Т и (0),..., (п); мы называем такие слова GLPn-словами. Модель ( Ил„/~; <о, Т, (0), (1),..., (п)) является системой ординальных обозначений для ординалов wn+i; здесь

Ul0 = 1, U)n+1 =

Отметим, что в указанной выше работе5 Л.Д. Беклемишева было показано, что конъюнкция всяких двух слов GLP-доказуемо эквивалентна некоторому GLP-слову. Это дает возможность естественным образом рассматривать полурешетки (ИУ~;А) и (И/П/~;Л).

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

В диссертации доказано, что элементарная теория модели (W/~; <о, Т, (0), (1),..., {п),...) неразрешима. Доказано, что при всех натуральных п > 3 неразрешимы элементарные теории моделей ( W„/~; <о, Т, (0), (1),..., (п)). При этом показано, что элементарная теория модели ( <о, Т, (0), (1), (2)) разрешима. Доказано, что язы-

ка первого порядка в полурешетках (И//~;А) и ( Л) достаточно

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

Цели работы.

1. Определить алгоритмическую сложность проблемы распознавания выводимости замкнутых формул для логик GLP и GLP„.

2. Исследовать вопрос о разрешимости элементарных теорий полурешетки GLP-слов и полурешеток СЬРп-слов.

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

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

Научная новизна. Результаты диссертации являются новыми и получены автором самостоятельно. Основные результаты диссертации состоят в следующем:

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

2. Для каждого натурального п проблема распознавания выводимости для замкнутых формул в логике GLP„ разрешима за полиномиальное время.

3. Полурешетка (ïf/~;A) и полурешетки (W„/~;A) для п> 2, имеют неразрешимые элементарные теории.

4. Полурешетка (Wi/~;A) обладает разрешимой элементарной теорией.

5. Элементарная теория алгебры ( <0, Т, (0), (1),..., (тг),...) неразрешима. Также для п > 3 неразрешима элементарная теория алгебры ( Wn/~] <0, Т, (0), (1),..., <п».

6. Алгебра ( <о, Т, (0), (1), (2)) обладает разрешимой элементарной теорией.

Методы исследования. В работе используются методы теории сложности вычислений, модальной логики и теории моделей. Для доказательства PSPACE-полноты замкнутого фрагмента логики GLP строится полиномиальное сведение языка булевых формул с кванторами к искомому. Полиномиальные разрешающие алгоритмы для замкнутых фрагментов GLP„ основаны на эффективном кодировании подмножеств предложенной К.Н. Игнатьевым12 универсальной модели Крипке для замкнутого фрагмента логики GLP. Мы доказываем неразрешимость элементарных теорий полурешеток GLP-слов, интерпретируя в них неразрешимую13 слабую монадическую теорию натуральных чисел в сигнатуре,

12K.N. Ignatiev. On strong provability predicates and the associated modal logics. The Journal of Symbolic Logic, 58(l):249-290, 1993.

13C.C. Elgot and M.O. Rabin. Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic, 31:169-181, 1966.

включающей в себя функцию следования и функцию Н(х) = 2х. Для доказательства разрешимости элементарной теории полурешетки (Wi/~; Л) строится ее интерпретация в теории структуры (шш;<,+). Результаты о неразрешимости элементарных теорий системы ординальных обозначений Беклемишева и ее фрагментов доказываются путем погружения теории класса всех пар линейных порядков на конечных множествах. Разрешимость элементарной теории модели <о, Т, (0), (1), (2)) доказывается при помощи построения ее интерпретации в разрешимой в силу результата JI. Бро14 слабой монадической теории ординала снабженного порядком и предикатом, задающим стандартную систему кофинальных последовательностей.

Теоретическая и практическая ценность. Работа имеет теоретический характер. Полученные результаты могут найти применение в математической логике и теоретической информатике. Результаты диссертации могут быть полезны специалистам, работающим в Математическом институте им. В.А. Стеклова РАН, МГУ им. М.В. Ломоносова, Институте математики им. С.Л. Соболева СО РАН, ПОМИ им. В.А. Стеклова РАН, ИППИ им. A.A. Харкевича РАН, Тверском государственном университете и др.

Апробация диссертации. Результаты диссертации докладывались на следующих семинарах и конференциях:

1. 1-ая и 2-ая международные конференции «International Workshop on Proof Theory, Modal Logic and Reflection Principles» в Барселоне, Испания, 16 апреля 2012 года и в Мехико, Мексика, 1 октября 2014 года, соответственно;

2. Международная конференция «Logic Colloquium 2013» в Эворе, Португалия, 22 июля 2013 года;

3. Международная конференция «Advances in Modal Logic 2012» в Копенгагене, Дания 22 августа 2012 года ;

4. Конференция «Ломоносов 2012» в Москве, Россия, 11 апреля 2012 года;

5. Семинар «Алгоритмические проблемы алгебры и логики» под руководством академика РАН С.И. Адяна в Москве, Россия, 23 октября 2012, 9 апреля 2013 года и 24 февраля 2015 года;

14L. Braud. Covering of ordinals. In Foundations of Software Technology and Theoretical Computer Science, pages 97-108, 2009.

Публикации. Основные результаты диссертации опубликованы в работах [1]—[3], из них все в журналах из перечня ВАК.

Структура диссертации. Работа состоит из введения, трех глав, содержащих 10 разделов, и списка литературы. Библиография содержит 33 наименования. Текст диссертации изложен на 83 страницах.

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

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

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

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

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

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

1. —>■ [п]<£>, где к<п\

2. {к)(р —¥ [п\(к)<р, где к < п.

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

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

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

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

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

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

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

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

<пф <=> вьр К V («)</?•

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

ч> ~ Ф вьр <р ■н- ф.

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

(п)[А]^ = {В [ В ~ (п)А),

[А]„ Л [В]„ = {С | С ~ А Л В}.

В главах 2 и 3 мы изучаем разрешимость элементарных теорий моделей ( И7~; Л, <0, Т, (0), (1), ...,<*>,...), (Т7„/~; Л, <„, Т, (0), (1),..., <п» и моделей, получаемых из них опусканием некоторых предикатов и функций. Отметим, что фактически из соображений технического удобства мы работаем не непосредственно с этими моделями, а с изоморфными моделями, носители которых составлены из слов в нормальной форме

(канонических представителей классов эквивалентности СЬР-слов по отношению

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

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

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

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

В главе 3 мы изучаем вопрос об разрешимости элементарных теорий моделей с носителями или и с сигнатурами могущими вклю-

чать лишь предикат <о, константу Т и функции вида (к). Отметим, что модели (<о, Т, (0), (1),... ,(к),...) и (<0, (0), (1),..., (п)) являются естественными конструктивными представлениями ординалов £о и соответственно.

Теорема 5. Пусть р, <7 и п — натуральные числа такие, что 0 < р и р + 1 < <7 < п. Тогда элементарные теории моделей (ИУ~; <о, (р), (?}) и (<о, (р), (д)) неразрешимы.

Модель (<о,Т, (0), (1),..., (к),...), в силу теоремы 5, имеет неразрешимую элементарную теорию. Также, из этой теоремы следует, что при всех п > 3 неразрешима элементарная теория модели (И^/~;<о,Т, (0), (!>,...,<«».

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

Теорема 6. При всех п > 2 у модели (<о,Т, (0), (1), (2)) разрешима элементарная теория.

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

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

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

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

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

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

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

Научное издание

Пахомов Федор Николаевич

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук на тему: Некоторые алгоритмические вопросы для полимодальных логик доказуемости

Заказ № 70-Р/07/2015 Подписано в печать 18.06.15 Тираж 100 экз. Усл. п.л. 0,6

ООО "Цифровичок", Москва, Большой Чудов пер., д.5 тел. (495)649-83-30

'' www.cfr.ru ; е-таП: zakpark@cfr.ru