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

• Автор: Пахомов, Федор Николаевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 2015
• Место защиты: Москва
• Количество страниц: 83 с.

Оглавление
Введение
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. □( ф) —> (П<р —> □■г/’);
2. □(□• <р) —» □
В 1976 году P.M. Соловей [27] доказал теорему об арифметической полноте логики GL. Модальная формула является теоремой логики GL, если и только если она переводится в теорему РА при любой подстановке арифметических предложений вместо пропозициональных переменных и расшифровке □ как Ргрд.
С середины 1970-х годов исследованию логики GL и других логик доказуемости было посвящено значительное число работ. В 1986 г.

Г.К. Джапаридзе рассмотрел [2] обобщение вЬ — логику вЬР, в которой вместо одной модальной связки □ используется занумерованное натуральными числами семейство модальных связок [0], [1],..., [л],... Джапаридзе доказал аналог теоремы Соловея об арифметической полноте, в котором связки [п] интерпретируются как доказуемость из аксиом РА с использованием выводов с с^-правилами с глубиной вложенности и-правил, не превосходящей п.
В настоящее время логика СЬР активно изучается в связи с ее применениями в ординальном анализе арифметических теорий [7]. Вопрос о характеризации формальных теорий ординалами является одним из центральных вопросов в теории доказательств. Исследования такого рода восходят к Р Генцену [19], который доказал непротиворечивость РА с помощью трансфинитной индукции до ординала е^. Применение логики СЬР основано на использовании замкнутых формул (формул без пропозициональных переменных) для обозначения арифметических теорий и для построения естественной системы ординальных обозначе-

ний для ординала ед = | п Е ш}.
п раз
В диссертации рассматриваются два круга алгоритмических вопросов, связанных с замкнутым фрагментом логики ОЬР.
1. Алгоритмическая сложность проблемы распознавания выводимости.
2. Разрешимость элементарных теорий алгебр естественных систем ординальных обозначений.
Вопрос об алгоритмической сложности проблемы выводимости для модальных логик изучался Р.Е. Ладнером [24]. Он показал, что многие классические модальные логики, включая 34, К, Т, обладают РБРАСЕ-полными проблемами распознавания выводимости формул. Хотя логика ОЬ не была рассмотрена в этой работе Ладнера, но использованный там метод легко позволяет получить аналогичный результат и для нее. В дальнейшем, И.Б. Шапировский доказал, что и логика СЬР

Рассмотрением случаев для внешней связки ф мы показываем, что вычисление с(ф) из кодов ранее рассмотренных формул занимает время 0{(р' • |(//|п+1). Полное вычисление с(<£>') занимает 0(|<^/|п+3) времени. Очевидно, что ОЬР Ь <р тогда и только тогда, когда
1зЕтрп(шп+1, Стр1п(ип+1, с(<р'))) = 1.
Тем самым, мы получаем требуемый алгоритм со временем работы
С>(МП+3). □