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

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

Крупский Николай Владимирович

НЕКОТОРЫЕ АЛГОРИТМИЧЕСКИЕ ВОПРОСЫ ДЛЯ ФОРМАЛЬНЫХ СИСТЕМ СО СВОЙСТВОМ ИНТЕРНАЛИЗАЦИИ ВЫВОДОВ

01.01.06 — математическая логика, алгебра и теория чисел

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

Москва — 2006

Работа выполнена на кафедре математической логики и теории алгоритмов Механико-математического факультета Московского государственного университета им. М. В. Ломоносова.

Научный руководитель:

Официальные оппоненты:

Ведущая организация:

доктор физико-математических наук, профессор Успенский Владимир Андреевич доктор физико-математических наук Беклемишев Лев Дмитриевич, кандидат физико-математических наук Вьюгин Михаил Владимирович Санкт-Петербургское Отделение Математического института им. В.А.Стеклова Российской Академии Наук

Защита диссертации состоится 7 апреля 2006 г. в 16 ч. 15 мин. на заседании диссертационного совета Д.501.001.84 в Московском государственном университете им. М. В. Ломоносова по адресу 119992, ГСП-2, Москва, Ленинские горы, МГУ, Механико-математический факультет, аудитория 14-08.

С диссертацией можно ознакомиться в библиотеке Механико-математического факультета МГУ (Главное здание, 14 этаж).

Автореферат разослан 7 марта 2006 г.

Ученый секретарь диссертационного совета Д.501.001.84 в МГУ доктор физико-математических наук, профессор В. Н. Чубариков

200 С ft

Общая характеристика работы Актуальность темы

Под свойством интернализации выводов для формальной системы ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Теории со свойством интернализации выводов являются предметом рассмотрения Второй теоремы Гёделя о неполноте формальной арифметики и играют центральную роль в многочисленных исследованиях в этом направлении (см., например, [1] 1 ). Типичным примером теории такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА позволяет определить инъективное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств

оказывается выразимым арифметической формулой Prf(x,y). При этом для любой арифметической формулы ¡р справедливо

РА I- <р -ФФ- РА Ь Prf(ñ, ripn) для некоторого натурального числа п.

(Здесь ñ — нумерал, соответствующий числу п, а — гёделевский номер формулы 1р.)

Множество всех теорем РА вида Prf(ñ, r<jP) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме — в виде их гёделевских номеров. В то же время он существенно проще множества всех теорем РА: отраженный фрагмент РА разрешим, в то время как множество всех теорем РА неразрешимо. Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами.

Факт простого устройства отраженного фрагмента для всех этих теорий уточняется как утверждение о его разрешимости, в то время как сама теория неразрешима. Такой подход неприменим в случае разрешимых теорий. Для

'[1|СморинскиЙ К. Теоремы о неполноте // В кн.: Дж. Барвайс, ред. Справочная книга по математической логике Ч IV М.-Hay

а

'х есть код вывода формулы с гёделевским номером у'

них вопрос о сравнении проблем разрешения самой теории и ее отраженного фрагмента до настоящей работы оставался открытым.

Примеры пропозициональных формализмов со свойством интернализации выводов построены в работах С.Н. Артёмова. Это логика доказательств LP [2J 2, [3] 3 и рефлексивная комбинаторная логика RCL_ [4] 4. В языках этих теорий присутствуют термы, играющие роль обозначений для выводов, и конструкция формул t:F, выражающая предикат доказательств "t есть вывод формулы F", причем формула F выводима в теории тогда и только тогда,

когда выводима формула t:F для некоторого терма £. Для логик LP и RCI__,

вопрос о сравнении сложности отраженного фрагмента (т.е. множества всех теорем вида t:F) и множества всех теорем теории остается актуальным, но требует другой формализации, так как обе системы оказались разрешимыми.

Разрешимость логики доказательств LP установлена в [5] 5 с помощью развитой в этой работе техники символических моделей. Оценка сложности разрешающего алгоритма для LP получена в [6J 6 : LP принадлежит классу Щ полиномиальной иерархии. До настоящей работы вопрос о сложности отраженного фрагмента логики доказательств LP, а также вопросы о разрешимости и сложности рефлексивной комбинаторной логики RCI__> и ее отраженного фрагмента не были изучены.

Определение понятия вывода в рефлексивной комбинаторной логике RCI__,

в качестве составной части содержит определение правильной построенности формул. Эта компонента является расширением правил типизации термов средствами комбинаторной логики Карри CI__„ для которой задачи проверки правильности типизации и восстановления типов термов разрешимы за полиномиальное время (см. [7] 7 ). Для RCL_, аналогами указанных задач являются задачи распознавания правильной построенности формул и вос-

2(2)Artemov S. Operational Modal Logic // Technical Report MSI 95-29,Cornell University, 1995

3[3]Abtemov S Explicit provability and constructive semantics // The Bulletin of Symbolic Logic, 7(l):l-36, 2001

4 [4] Артёмов С H Подход Колмогорова и Гёделя к интуиционистской логике и работы последнего десятилетия в этом направлении // Успехи матем. наук, 2004, 59, вып. 2 (356), 9-36

5[5]Mkrtychev A Models for the logic of proofs // Lecture Notes in Computer Science, v. 1234, 1997, 266-275

»[6jkuznets R On the complexity of explicit modal logics // Lecture Notes in Computer Science, v. 1862, 2000, 371-383

t[7]Troelstra A.S., Schwichtenberg H. Basic proof theory // Cambridge: Cambridge Univ. Press, 1996

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

Цель работы

Целью работы является доказательство разрешимости и получение оценок сложности для ряда алгоритмических проблем, связанных с отраженным фрагментом Я1_Р логики доказательств 1.Р (оценить сложность разрешения),

рефлексивной комбинаторной логикой РС1__, и ее отраженным фрагментом

(доказать разрешимость и оценить сложность разрешения) и задачей типизации термов средствами ИСЬ ^ (предложить полиномиальный по времени алгоритм восстановления типов).

Основные методы исследования

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

Научная новизна

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

1. Пусть 1_Р(С5) обозначает вариант логики доказательств 1_Р с ограниченным правилом (ТУес) - дополнительно требуется, чтобы его заключение принадлежало заданному конечному множеству формул С5. Показано, что отраженный фрагмент логики доказательств иР(С5) есть теория одной символической модели. В качестве следствий установлен

ряд утверждений, упрощающих поиск выводов в 1_Р, в частности, следующий вариант дизъюнктивного свойства:

1_Р (- V 1.Р I- или 1.Р I- Ь.в.

2. Установлено, что отраженный фрагмент логики доказательств 1.Р принадлежит классу ИР. Эта верхняя оценка ниже известной верхней оценки для всей логики 1_Р. Аналогичная оценка доказана также для более широкого фрагмента — множества всех теорем 1.Р, являющихся монотонными булевыми комбинациями квазиатомарных формул.

3. Для рефлексивной комбинаторной логики (-Ю__, предложено явное определение типов. Доказана единственность типизации термов средствами РЮ__,. Установлено, что задачи восстановления типов и проверки правильной построенности формул для ИС1__, разрешимы за полиномиальное время.

4. Предложено секвенциальное исчисление, формализующее отношение

выводимости из гипотез в рефлексивной комбинаторной логике ЯС1__,.

Показано, что правило сечения в нем устранимо. Отсюда следует, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.

5 Доказано, что отношение выводимости из гипотез в логике 13С1__, разрешимо и РБРАСЕ-полно.

Апробация работы

Результаты диссертации докладывались на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ (руководители семинара — академик РАН, профессор С И. Адян и профессор В.А Успенский, 2005 г.), на семинаре лаборатории математической логики Санкт-Петербургского Отделения Математического института им. В.А.Стеклова РАН (2005 г.), на семинаре "Логические проблемы информатики"(руководители семинара — профессора С Н. Артемов, МР Пентус и доценты В.Н. Крупский. ТЛ. Яворская, неоднократно), а также на XXIV Конференции молодых ученых Механико-математического факультета МГУ (2002 г.).

Публикации

Результаты диссертации опубликованы в работах [1-5], список которых приводится в конце реферата.

Структура и объем работы

Работа состоит из введения, трех глав и списка литературы Объем диссертации — 80 страниц, список литературы содержит 19 наименований.

Краткое содержание диссертации

Во введении приводится обзор работ по исследуемой теме и кратко форму» лируются основные результаты диссертации

Глава 1 посвящена изучению отраженного фрагмента Р1_Р логики доказательств СР. Параграф 1.1 носит вспомогательный характер. В нем приведены 1 основные определения и известные свойства символических моделей для ло-

гики доказательств [_Р (см. [З]3, [б]5).

Язык логики доказательств 1.Р содержит два сорта выражений: термы (Тт) и формулы (Рт). Термы строятся из переменных по доказательствам 5 х, и констант по доказательствам с, при помощи функциональных символов

!, + и • :

Тт ::= хг | с, | (\Тт) | (Тт + Тт) | (Тт ■ Тт).

' Пусть вУаг — {5о, ...} - множество пропозициональных переменных.

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

Рт 5Уаг | (-чРт) | (Рт А Рт) | (Рт V Рт) | (Рт -> Рт) | (Тт : Рт).

Формулы вида где t б Тт, Р € Рт, называются квазиатомарными формулами.

Логика доказательств 1.Р задается исчислением с аксиомами А0-А4 и правилами вывода (МР) и (ТУес):

АО Аксиомы классической логики высказываний в языке 1.Р, А1 *:Р —Р,

А2 t:(F —►(?)—> (s:F — (t ■ s):G),

A3 t:F -> (i + s):F, s:F (t + s):F,

A4 t:F —>H:(t:F).

(MP) F -л G, F b G,

(Nec) t- а А, где с — константа, а А — аксиома одного из видов А0-А4.

Спецификацией констант CS называется конечное множество формул вида с-А, где с есть константа по доказательствам и А есть одна из аксиом А0-А4. Обозначим через LP(CS) фрагмент LP с аксиомами А0-А4, правилом {MP) и следующим ограниченным видом правила Nec:

(Neccs) Ь с.А для с.А € CS.

Определение 1.1.2 Функция * : Тт —> сопоставляющая каждому LP-терму множество LP-формул, называется свидетельской функцией, если она удовлетворяет следующим условиям:

1. Если (F —> G) € *(t) и F € *(s), то G 6 *(< • з).

2. *(i) U *(s) С *(t -I- s).

3. Если F е *(i), то t:F € *(!i)-

Определение 1.1.3 Моделью называется тройка М = (v, *, ¡=), где v — оценка пропозициональных переменных, т.е. отображение v : SVar —> {True, False], * — свидетельская функция, a f= есть отношение истинности, определяемое по первым двум компонентам М следующим образом:

1. М |= S v{S) = True для 5 € Svar,

2. М \=-iF M^F\

3. М \= F /\G М )= F а М \= G\

4. M\=FVG М \= F или М (= G;

5. M^F->G 4=> М F или М \=G]

6. M\=t:F F 6 *(i);

Определение 1.1.5 Модель М = (и, *, |=) называется рефлексивной, если F € *(£) влечет Л/ (= F.

Пусть дана спецификация констант CS. Модель М называется CS-моделью, если М (= Д С5. Логика LP(CS) полна в классе всех рефлексивных CS-моделей: формула F истинна во всех рефлексивных CS-моделях тогда и только тогда, когда LP(CS) Ь F (см. [5]5).

Определим частичный порядок на множестве всех моделей. Пусть М — (v, *, }=) и М' = (т/, *', (=') — модели. Тогда М < М', если выполнены два

условия: «(5) = Тгие влечет у'(Б) = Тгие для каждой переменной 5 € ЯУаг, и *(£) С *'(£) для каждого терма Ь £ Тт. В параграфе 1.2 доказывается существование наименьшей С5-модели.

Теорема 1.2.5 Для каждой спецификации констант СБ в классе всех рефлексивных С5-моделей существует наименьший элемент М. Для этой модели выполняется: М |= ЬР ЬР(С£>) Ь ЬР.

В качестве следствия устанавливается ограниченный вариант дизъюнктивного свойства логики доказательств ЬР.

Следствие 1.2.7

ЬР I- ti-.Fi V ... V о ЬР I- ti-.Fi или ... или ЬР I-

В параграфах 1.3, 1.4 предлагается аксиоматическое описание отраженного фрагмента логики доказательств ЬР и доказывается, что отраженный фрагмент логики доказательств принадлежит классу сложности NP.

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

(С1) Ь.(Р - С), з-Р Ь

(С2) Ь.Р Ь (* + в)Р, з:Р Н (« + з)Р-(СЗ) ь.Р I- \Ь.{ЬР).

и правилом (N60) в том же объеме, что и для исчисления ЬР.

Теорема 1.3.1 (пункт 2) ЬР I- ЬЯ С Ь ЬР.

Теорема 1.4.2 ИЬР принадлежит классу сложности МР.

Установленное выше дизъюнктивное свойство ЬР позволяет распрострет нить эту оценку на более широкий класс теорем ЬР. Обозначим через РЬРд,у множество всех теорем исчисления ЬР, построенных из квазиатомарных формул с помощью связок А, V.

Теорема 1.4.4 РЬРАу принадлежит классу сложности ИР.

В главе 2 рассматриваются задачи распознавания правильной построен-ности формул рефлексивной комбинаторной логики РС1___ и типизации термов ее средствами. Основные определения приведены в параграфе 2.1.

Пусть ро,р1,... — пропозициональные (или типовые) переменные, к, в, о, с и хо,х\,... — две группы идентификаторов. Множества всех термов (Тт) и всех формул (Рт) языка РЮ__, определяются следующей грам-

матикой:

Тт х?т | кГт | \ оРт | <1Рт \ </т |! Тт \ Тт ■ Тт, Рт :■- р, | Ртп Рт I Ттп.Гтп.

Переменные - это термы вида х[ш. Константы - это термы видов кРт, зРт, </т, АРт или срт. Элементы множества Тт и Рт называются выражениями. Множество всех всех ассоциированных подвыражений АЯиЬ(е) для выражения е € Тт и Рт состоит из всех его подтермов и подформул, включая подтермы и подформулы всех верхних индексов. Размером выражения е € Тт и Рт называется мощность множества АЯьЬ(е).

Формула Р называется правильно построенной (п.п.ф.), если суждение иР - п.п.ф." выводимо в исчислении РСЬ-м^. Терм £ называется типизуе-мым, если суждение "< : Р - п.п.ф." для некоторой формулы Р выводимо в исчислении Правила исчисления РСЬ-игГ таковы (см [4]4):

, 0 в -п.п.ф. Р- п.п.ф.

1. р, - п п.ф 2. —-—-— 3.

► <7-п.п.ф. п.п.ф.

Ь: Р - п.п.ф. г ^ (б -> Г) - п.п.ф.

4. -,.- „-—-г* 5.

6.

:(Ь:Р - п.п.ф. ' —»((?—► F)) - п.п.ф.

_(Р -> (в -» Я)) -> ((^ —>(?)—> (.Р —> Я)) - п.п.ф._

: ((р _> (в -у Я)) ((Г -> С) (.Р — Я))) - п.п.ф.

Р, (9, и:{Р у:Р- п.п.ф.

7.

8.

(ии): С? - п.п.ф. Г, (?, и:(Р О), у:Р - п.п.ф.

р-(-) 0; : —»С) —> (ь:Р («и): С))) - п.п.ф

Р, ¿:.Р-п.л.ф. п.п.ф.

* 10.

!г:(*:Р) -п.п.ф. ' с"-*«"! -►!<:(<: Г)) -п.п.ф.

П П П-Ф

б - п.п.ф.

Параграф 2.2 посвящен упрощению определения п.п.ф. языка !ЗС1__,. В нем

показано, что правило И является устранимым (лемма 2.2.1), а остальные правила допускают следующие упрощения: в правилах 5 и 6 посылки можно заменить на "Р, б - п.п.ф." и "Р, С,Н - п.п.ф." соответственно, и в правилах

4, 7, 8, 9, 10 посылки "F - п.п.ф." и "С - п.п.ф." можно опустить. Все эти изменения не меняют множества выводимых суждений (следствия 2.2.3 и 2.2.7).

Теорема 2.2.8 1. Если терм t является ассоциированным подтермом п.п.ф., то он типизуем. Более того, формула G, такая что формула t : G является п.п.ф., единственна и также правильно построена. 2. Каждая ассоциированная подформула п.п.ф. является п.п.ф..

Согласно этой теореме, ассоциированным подтермам правильно построенных формул можно однозначно сопоставить формулы, обозначающие их типы. Условимся писать сопоставленные формулы в виде верхних индексов у термов, а также рекурсивно продолжать разметку внутрь верхних индексов. Так задается отображение разметки (-)г, определенное на всех п.п.ф. и ти-пизуемых термах. Размеченные формулы вида F1", где F — п.п.ф., являются

полными обозначениями для типов в RCI__,. П.п.ф. являются сокращенными

обозначениями для тех же типов. В параграфах 2.3, 2.4 предлагается другое,

явное определение типов для RCI__, в виде отдельного исчисления RCLT-wf и

доказывается эквивалентность двух определений: RCLT-wf Ь (X type) тогда и только тогда, когда X — Fr для некоторой п.п.ф. F (теорема 2.4.2).

В параграфе 2.5 оценивается сложность следующих задач:

Проблема типизации термов. По терму t выяснить, типизуем ли он, и, в случае положительного ответа, восстановить tr.

Проблема восстановления типов в формулах. По формуле F выяснить, является ли она правильно построенной, и, в случае положительного ответа, восстановить F1".

Исходные данные (выражение е) поступают на вход алгоритмов в DAG-представлении, т.е. в виде размеченного ориентированного графа без циклов и без повторяющихся идентичных подграфов. Количеством вершин равно размеру выражения. Вершины соответствуют ассоциированным подвыражениям выражения е и помечены их главными символами, причем для вершин ni,ri2, соответствующих выражениям е^ег G ASub(e), наличие пути из щ в п2 эквивалентно условию е2 € ASub(ei). Результы работы алгоритмов представляются аналогичным образом.

Теорема 2.5.5 Проблемы типизации термов и восстановления типов в

формулах для RCI__, разрешимы за полиномиальное (от размера входных

данных) время.

Глава 3 посвящена изучению отношения выводимости из гипотез в рефлексивной комбинаторной логике ЯС1__,. Аксиомами ИС1__, являются все

правильно построенные формулы одного из видов (А1) - (А6).

(А1) г-.р-+р,

(А2) -*

(АЗ) ((?-> F)),

(А4) ^О ■НП-^С^Г-Н» ; ((/Р —> (С—» Я)) - ((^ С) (^ Я))),

(А5) <л('-е)-с-<"-)«'):(и:(Р-»<?) ->■ (У:Р-~> (иь) :С))),

(А6) с "-«»> <« ч: (и: ^ ->(!и): (и:

Правило вывода:

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

В параграфе 3.1 предлагается секвенциальная формулировка рефлексивной комбинаторной логики. Множества всех размеченных термов (ЬТт) и всех размеченных формул (ЬРт) определяются следующей грамматикой:

ЬТт ::= х^'т \ | з1Рт | оЬРт | аР'т | | (! ЬТт)ЬРт | (ЬТт ■ ЬТт)1Тт, ЬРт ::= р, | LFm -> LFm | ЬТт: ЬРт.

Рассматриваются секвенции вида Г F, где Р € ЬРт, а Г — конечное мультимножество размеченных формул. Секвенция называется правильно построенной, если F и все члены Г имеют вид С, где (3 — п.п.ф.. Секвенциальный вывод назовем правильно построенным, если все секвенции в нем правильно построены. Секвенциальное исчисление РС1Л"с определяется следующим образом:

Аксиомы: все секвенции вида Р, Г =Ф- Р, где Р есть типовая переменная р< или размеченная формула вида : 6?.

Правила:

г=»^ С, Г=>Я Р —> С, Г Я

Р, Г, г =» в Р, г =>с

(ЬС)

Г =>Р

г, г' с

(С««)

(Л!)

х>

(Д.) Г=»Л (Я *)

Правило (7? г) имеет специальный вид. Буква г в нем означает один из идентификаторов к, 5, й, о, с, а формула 1А : А имеет вид соответствующей аксиомы (А2)-(А6) исчисления ЯС1__,. Вывод Т> зависит от Г, А и является стандартным (фиксированным) выводом без сечения секвенции Г => А. Правило утверждает, что этот конкретный вывод может быть за один шаг продолжен до вывода секвенции Г => : А.

Пусть ()° : ЬРт —» Ртп обозначает перевод, который удаляет верхние индексы у всех ассоциированных подтермов видов (Н)р и (£1 •

Теорема 3.1.4 1. Если Г Р, то секвенция Р" имеет правильно построенный ЯСиГс-вывод.

2. Если секвенция Г =>• Р имеет правильно построенный ЯС1Л~с-вывод, то

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

Теорема 3.2.5 Каждый вывод в РС1_Тс можно преобразовать в вывод той же секвенции, но без сечения. Если выводимая секвенция правильно построена, то преобразованный вывод (без сечения) - также правильно построрн

Параграфы 3.3 и 3.4 посвящены доказательству разрешимости отношения выводимости из гипотез в исчислении ЯСЬТо и оценке сложности разрешающего алгоритма.

Теорема 3.3.6 Множество секвенций, выводимых в исчислении ЯС1Л"с, и отношение выводимости из гипотез в исчислении РС1__, разрешимы.

Далее показывается, что проблема выводимости секвенций в исчислении

RCLTg и проблема выводимости формул из гипотез в исчислении RCI__, лежат

в классе сложности PSPACE (теорема 3.4.3 и следствие 3.4.4). Эта оценка комбинируется с известной нижней оценкой сложности для импликативного фрагмента интуционистской пропозициональной логики [8] 8 , что позволяет установить PSPACE-полноту проблемы выводимости для RCI__

Теорема 3.4.5 Проблемы выводимости секвенций для исчисления RCLTg и выводимости формул для исчисления RCI__, являются PSPACE-полныии.

Теорема 3.4.7 Задача распознавания выводимости формул вида t:F в исчислении RCI__, разрешима за полиномиальное время (от размера формулы).

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

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

1. Н.В Крупский. Минимальные модели и сложность фрагментов логики доказательств // Вестник московского университета, сер. 1., Математика, Механика, 2006, №1 52-53.

2. Н.В. Крупский. О сложности фрагментов логики доказательств // В сб.: Труды XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В. Ломоносова, 2002, 96-98.

3 N. Krupski On the complexity of the reflected logic of proofs // CUNY Ph.D Program in CS Technical Reports, TR-2003007, 2003, 12 p.

4 N Krupski Typing in Reflective Combinatory Logic // CUNY Ph.D Program in CS Technical Reports, TR-2005013, 2005, 24 p.

5. Н.В. Крупский О синтаксисе рефлексивной комбинаторной логики // Деп. в ВИНИТИ, М12-В2005, М. ВИНИТИ, 2005, 29 с.

8|8]Statman Л Intuitionistic prepositional logic is polynomial-space complete // Theoretical Cornput Sci 9, 1979, 67-72

Подписано в печать 02.03.06 Формат 60x90 1/16. Усл. печ. я.

Тираж /00ЭКЗ, Заказ //

Лицензия на издательскую деятельность ИД В 04059, от 20.02.2001г.

Отпечатано с оригинал-макета на типографском оборудовании механико-математического факультета

XOOGf\ 5\\<o

5f I*

0.1 Введение.

1 Отраженная логика доказательств.

1.1 Основные определения.

1.2 Конструкция наименьшей модели

1.3 Отраженный фрагмент логики доказательств.

1.4 Сложность фрагментов логики доказательств.

2 Типизация термов в рефлексивной комбинаторной логике.

2.1 Определение правильно построенных формул RCL—.

2.2 Типизация подтермов.

2.3 Типы в RCU.

2.4 Соответствие между правильно построенными формулами и типами.

2.5 Восстановление типов.

3 Выводимость в рефлексивной комбинаторной логике.

3.1 Выводимость из гипотез в RCL-*.

3.2 Устранение сечения в RCLTg.

3.3 Разрешимость RCLTg.

3.4 Оценки сложности.

Под свойством интернализации выводов для формальной системы Т ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Типичным примером формализма такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА (см. [15], [11]) позволяет определить инъек-тивное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств их есть код вывода формулы с гёделевским номером у" оказывается выразимым арифметической формулой Prf(x,y). При этом для любой арифметической формулы ip справедливо

PA b tp PA b Pr/(n, rip~l) для некоторого натурального числа п.

Здесь п — нумерал, соответствующий числу п, а г(р~] — гёделевский номер формулы ip.)

Множество всех теорем РА вида Prf(n,rip~]) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме и с дополнительной информацией про их выводы. В то же время он существенно проще множества всех теорем РА. Естественный выбор деталей кодирования приводит к выражению предиката доказательств посредством Ai-формулы. Это обеспечивает разрешимость отраженного фрагмента, в то время как множество всех теорем РА неразрешимо.

Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами. Факт разрешимости отраженного фрагмента теории Т является следствием разрешимости отношения d сеть вывод формулы </?" для теории Т, а сама теория Т неразрешима ввиду существенной неразрешимости РА (см. [15]). Поэтому отраженный фрагмент устроен проще всей теории Т. Заметим, что это рассуждение использует факт неразрешимости теории Т и неприменимо в случае разрешимых теорий. Для ряда разрешимых формализмов вопрос о сравнении проблем разрешения для теории и ее отраженного фрагмента остается открытым.

Логика доказательств LP С.Н. Артёмова [1], [2], [3], [5], [6] является примером разрешимой пропозициональной логики со свойством интернализации выводов. В языке LP присутствуют выражения двух видов — термы, или полиномы доказательств (proof polynomials), и формулы. Термы строятся из переменных и констант первого вида ("по доказательствам") с помощью унарной операции "!" (верификация) и бинарных операций "•" (аппликация, применение modus ponens),"+" (объединение доказательств). Формулы строятся из пропозициональных переменных (второго вида) с помощью булевых связок и дополнительного конструктора квазиатомарных формул ":", действующего по следующему правилу: если t — терм, a F — формула, то t:F является формулой.

Логика доказательств LP задается следующим исчислением: Аксиомы:

АО Аксиомы классической логики высказываний в языке LP, А1 t:F F,

А2 t:(F G) -> (s:F (t • s):G), A3 tF + s)F, sF + s)F, A4 tF->\t:{tF). Правила вывода :

MP) F G, F h G,

Nec) Ь с: А, где с — константа, а А — аксиома одного из видов А0-А4.

Забывающей проекцией называется перевод формул языка LP в модальный язык, получающийся в результате замены всех вхождений "t:" на модальность □. Как показано в работах [1], [3] (Теорема о реализуемости), забывающая проекция логики LP, т.е. образ множества всех теорем, совпадает с логикой абстрактной доказуемости S4 Гёделя. В этом смысле логику доказательств LP можно считать детализированным, или явным (explicit), вариантом S4.

Арифметическая семантика для языка LP описана в [1], [3]. Она позволяет интерпретировать символ ":" как многозначный предикат доказательств для формальной арифметики РА, т.е. как арифметическую Ai-формулу х есть код конечного множества, среди элементов которого есть РА-вывод формулы с кодом у".

При этом символам !,-,+ соответствуют вычислимые операции на конечных множествах выводов, специфицированные аксиомами А2-А4, а константам по доказательствам — конечные множества, содержащие РЛ-выводы арифметических переводов аксиом LP. В [3] доказано, что логика доказательств LP корректна и полна относительно арифметической семантики.

Как отмечено в [5], свойство интернализации выводов является фундаментальным свойством LP. Имеет место (см. [3]) эквивалентность:

LP I- F LP h t:F для некоторого терма t.

Синтаксическая структура терма t из правой части эквивалентности задает последовательность операций, позволяющую построить вывод формулы F, существование которого утверждается в левой части. Соответствующие действия производятся с конечными множествами

LP-выводов, в результате чего получается конечное множество, содержащее вывод формулы F. Эквивалентность не нарушится, если дополнительно потребовать, чтобы терм t не содержал переменные и операцию +, а операция ! применялась в нем только к константам. В этом случае структура (дерево подтермов) терма t изоморфна дереву вывода формулы F из аксиом А0-А4 с помощью правил (MP) и (Nec).

Разрешимость LP установлена в [16] с помощью развитой в этой работе техники символических моделей для логики доказательств. Оценка сложности разрешающего алгоритма из [16] получена в [12]: LP принадлежит классу Щ полиномиальной иерархии. Таким образом оказывается, что LP проще, чем ее забывающая проекция 54, т.к. последняя PSPACE-иолш [13]. Нетривиальной нижней оценки сложности LP неизвестно. До настоящей работы вопрос о сложности отраженного фрагмента логики LP, т.е. множества всех теорем LP вида t:F, также не был изучен.

Родственным LP примером типовой комбинаторной логики со свойством интернализации выводов является описанная в [5] рефлексивная комбинаторная логика RCI>. Она является расширением типовой комбинаторной логики CI„ (см. [19]), допускающим погружение суждений о типизации вида "t является термом типа F" в систему типов при помощи дополнительного конструктора типов t: F. Аналогичный конструктор типов присутствует в интуционистской теории типов (ITT, см. [9], [14]), но в этой теории типы вида t : F оказываются тривиальными в следующем смысле: каждый непустой ITT-тип t: F содержит единственный канонический элемент, один и тот же для всех типов такого вида. В отличие от ITT, непустой тип t: F в RCL> нетривиален. Как показывается в настоящей работе (см. главу 2), он населен термами t\ хранящими полную информацию о суждении "t является термом типа F", и само сужение может быть однозначно восстановлено как тип терма t'.

Для рефлексивной комбинаторной логики также справедлива (см. [5]) эквивалентность:

RCI» Ь F RCI> Ь t:F для некоторого терма t, причем по терму t из правой части удается однозначно восстановить формулу F и построить ее вывод (см. главу 2).

Приведем определение формальной системы RCL из [5]. В нем совместной индукцией определяются два суждения: "F есть правильно построенная формула (п.п.ф.)" и "F выводима из гипотез F\,., Fn". Правильно построенные формулы играют роль обозначений для типов. Суждение о выводимости можно интерпретировать как условное суждение "непустота типов Fi,.,Fn влечет непустоту F". Формализуемое этим суждением понятие выводимости использует единственное правило вывода modus ponens, причем постулировано, что все аксиомы есть п.п.ф., а правило modus ponens сохраняет свойство "быть п.п.ф.".

Язык RCL>, правильно построенные формулы и выводимые формулы определяются совместной индукцией.

1. Язык RCL-+ содержит пропозициональные переменные Po,Pi,.- и пропозициональную связку "—Каждая пропозициональная переменная есть (атомарная) формула.

2. Если S и Т — формулы, то S —* Т — также формула.

3. Для каждой формулы F фиксируется свой набор дока-зуемостных переменных xo,%i,. • ■ ■ Если х это переменная типа F, то x:F есть формула. Здесь и ниже утверждения "t:F есть формула" и "t есть терм типа F" используются как синонимы.

4. Каждая из аксиом А1-А6 является формулой.

А1. Для каждых формул А и t:A есть аксиома t:A А.

А2. Для каждой формулы А —(В —>■ А) фиксируется константа к и аксиома к : (А (В А)). A3. Для каждой формулы (А —► (В -> С)) ((А —> Б) —> (А —> С)) фиксируется константа s и аксиома s . [(i4 {В С)) ((Л В) (Л С))].

А4. Для каждой формулы —» Л фиксируется константа d и аксиома d : (Ы А).

А5. Если А, В, и : (А В), v : А — формулы, то (и • v) : В также формула, причем для формулы и:(А —> В) —» {v.А —» (и • v):B) фиксируется константа о и аксиома о : [и:(А В) ('и:А (и • *;):£)]. А6. Если А и t: А формулы, то ! t : t: А также формула, причем для формулы t:A —>\t:t:A фиксируется константа с и аксиома с : (Ы ->\t:t:A). 5. Каждая доказуемая из гипотез формула есть правильно построенная формула. Гипотезы — это произвольное конечное множество Г формул. Вывод из гипотез Г есть конечная последовательность формул, каждая из которых есть либо гипотеза из Г, либо аксиома, либо следует из предшествующих в данной последовательности по правилу modus ponens:

А->В А В '

Выражение Г b F означает, что существует вывод из Г, содержащий F"

Детальный анализ, некоторое уточнение и упрощение этого определения проделаны в главах 2, 3 настоящей работы. Сейчас же отметим, что в [5] отсутствовало явное определения типов и термов для системы RCI>, что оставляло открытым вопрос о том, что именно обозначают п.п.ф. До настоящей работы не были исследованы проблема разрешения и сложность логики RCI,, а также сложность задачи типизации термов ее средствами.

Целью работы является доказательство разрешимости и получение оценок сложности для ряда алгоритмических проблем, связанных с отраженным фрагментом RLP логики доказательств LP, рефлексивной комбинаторной логикой RCIее отраженным фрагментом и задачей типизации термов средствами RCIДля этого предложены простые дедуктивные описания RLP и RCIдопускающие эффективные алгоритмы поиска выводов формул.

Основные результаты работы таковы. •

• Пусть LP(CS') обозначает вариант логики доказательств LP с ограниченным правилом (Nec) — дополнительно требуется, чтобы его заключение принадлежало заданному конечному множеству формул CS. Показано, что отраженный фрагмент логики доказательств LP(CS') есть теория одной символической модели. В качестве следствий установлен ряд утверждений, упрощающих поиск выводов в LP, в частности, следующий вариант дизъюнктивного свойства:

LP Ь s:F V t:G & LP b s:F или LP h t:G.

• Установлено, что отраженный фрагмент логики доказательств LP принадлежит классу NP. Эта верхняя оценка ниже известной верхней оценки для всей логики LP. Аналогичная оценка доказана также для более широкого фрагмента — множества всех теорем LP, являющихся монотонными булевыми комбинациями квазиатомарных формул.

• Для рефлексивной комбинаторной логики RCI„ предложено явное определение типов. Доказана единственность типизации термов средствами RCI—Установлено, что задачи восстановления типов и проверки правильной построенности формул для RCI> разрешимы за полиномиальное время.

• Предложено секвенциальное исчисление, формализующее отношение выводимости из гипотез в рефлексивной комбинаторной логике RCL>. Показано, что правило сечения в нем устранимо. Отсюда следует, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.

• Доказано, что отношение выводимости из гипотез в RCL разрешимо и PSPACE-полио.

Дальнейшее изложение придерживается следующего плана. Глава 1 посвящена изучению отраженного фрагмента RLP логики доказательств LP. Параграф 1.1 содержит определение символических моделей для языка логики доказательств и описание их основных свойств. В параграфе 1.2 доказывается существование наименьшей символической модели. Как следствие, устанавливается ограниченный вариант дизъюнктивного свойства логики доказательств. В параграфе 1.3 предлагается аксиоматическое описание отраженного фрагмента RLP логики доказательств LP. В параграфе 1.4 доказывается, что отраженный фрагмент логики доказательств RLP принадлежит классу сложности NP. Эта оценка распространяется также на более широкий класс теорем LP, имеющих вид монотонных булевых комбинаций квазиатомарных формул.

В главе 2 рассматривается задача типизации термов средствами рефлексивной комбинаторной логики RCI>. Параграфы 2.1, 2.2 посвящены упрощению определения правильно построенных формул языка RCL>. В параграфах 2.3, 2.4 предлагается явное определение типов для RCI, в виде отдельного исчисления RCLT-wf и показывается, что правильно построенные формулы являются корректными сокращенными обозначениями для типов. Устанавливается также, что все термы, входящие в состав правильно построенных формул, типизуемы единственным образом. В параграфе 2.5 рассматриваются проблемы типизации термов и восстановления типов в формулах. Доказывается, что обе они разрешимы за полиномиальное время.

Глава 3 посвящена изучению отношения выводимости из гипотез в рефлексивной комбинаторной логике. В параграфе 3.1 предлагается секвенциальная формулировка рефлексивной комбинаторной логики (исчисление RCLTg) и показывается ее эквивалентность исходному исчислению RCI—». В параграфе 3.2 устанавливается устранимость правила сечения в исчислении RCLTg- Параграфы 3.3 и 3.4 посвящены доказательству разрешимости отношения выводимости из гипотез в исчислении RCI—► и получению верхней оценки сложности (PSPACE) для разрешающего алгоритма. Эта оценка комбинируется с известной нижней оценкой сложности для импликативного фрагмента интуционистской пропозициональной логики, что позволяет доказать PSPACE-полноту проблемы выводимости для RCI— Здесь же доказывается, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.

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

Теорема 3.3.6 Множество секвенций, выводимых в исчислении

RCLTG, ^ отношение выводимости из гипотез в исчислении RCI >

разрешимы. Доказательство. Согласно лемме 3.3.3, секвенция V =^ F выводи ма в RCLTG тогда и только тогда, когда у секвенции set{V) =» F

существует монотонный RCLT'(^ -вывoд, в котором антецедент каждой

секвенции не содержит повторяющихся размеченных формул. Рас смотрим минимальный такой вывод. Он является последовательно стью секвенций, удовлетворяющих следующим условиям:

• все секвенции попарно различны и составлены из слабых под формул некоторых размеченных формул из множества Г U {F}

(лемма 3.3.5);

• кратность формул в антецедентах секвенций равна 1. Множество последовательностей, удовлетворяющих указанным усло виям, конечно и эффективно восстанавливается по секвенции Г =^ F.Для проверки ее выводимости достаточно выяснить, есть ли сре ди этих последовательностей монотонный КС1Т(^-вывод секвенции

set(r) => F. Согласно теореме 3.1.4, Г I-RCL_, F тогда и только тогда, когда 1)

все формулы из множества r u { F } правильно построены и 2) секвен ция Г'" => F^ обладает правильно построепным выводом в RCLTG. Первое из условий разрешимо по теореме 2.5.5, причем его выполне ние уже гарантирует суш,ествование и правильпую построенность се квенции Г^ =4> F''. Т.к. правило сечения в системе RCLTG устранимо,

то, по лемме 3.1.3, каждая выводимая в нем правильно построенная

секвенция имеет правильно построенный вывод тоже. Поэтому доста точно проверять лишь выводимость секвепции Г^ =^ JP^ в исчислении

RCLTG, ЧТО МОЖНО сделать изложенным выше методом. Замечание. Отметим, что результат о разрешимости (теорема 3.3.6)

может быть доказан тем же способом, основанным на более слабом

варианте леммы 3.3.3 (без условия монотонности и с более слабым

ограничением на кратность формул в антецедентах). Лемма 3.3.3 в

полном объеме будет использована ниже при доказательстве верхней

оценки сложности разрешаюш;их алгоритмов. 3.4 Оценки слож;ности. Покажем, что задача распознавания выводимости секвенций для ис числения RCLTG И задача распознавания выводимости из гипотез для

исчисления RCI > лежат в классе PSPACE. Онределение 3.4.1 Условимся называть размером секвенции сум му размеров всех входяш;их в нее размеченных формул. Лемма 3.4.2 Рассмотрим семейство всех минимальных монотон ных КаЛ^-выводов без повторяющихся размеченных формул в ан 72 тецедентах секвенций. Существуют полиномы qi и 2^ такие, что

глубина каждого из этих выводов не превосходит qi{n), а размеры

входящих в вывод секвенций не превосходят q2{n), где п — размер

выводимой секвенции. Доказательство. Возьмем произвольный КС1Т'(^-вывод секвенции размера п, удо влетворяющий условиям теоремы, и рассмотрим путь в дереве выво да от корня к листьям:

Разобьем этот путь на максимальные отрезки, внутри которых Г^

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

секвенции, что не превосходит п. Количество отрезков разбиения не

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

длина пути ограничена величиной v?. Рассмотрим произвольную секвенцию из RCLTQ-вывода секвенции

размера п, удовлетворяющего условиям теоремы. Количество фор мул в ней ограничено величиной п + 1, поскольку антецедент не со держит повторений. Размер каждой формулы в данной секвенции

ограничен величиной п. Таким образом, размер секвенции ограни чен величиной п{п + 1). Теорема 3.4.3 Мноснсество всех выводимых в исчислении RCLTG

секвенций леоюит в классе PSPACE. Доказательство. Пусть qi,q2 — полиномы из леммы 3.4.2. Рассмот рим следующую игру двух лиц, (I) и (II). Начальной конфигурацией игры (6о) является секвенция Г =^ F размера п. Ходы игроков че редуются. Игрок (I) предлагает одну или две секвенции размера, не

превосходящего q2{Ti), а игрок (II) выбирает одну из них. Партия пре кращается, если игрок (II) выбрал аксиому исчисления RCLT'^ ^ или

количество ходов игрока (И) превысило qi{n). Пусть Wi - ходы иг рока (I), а bj - ходы игрока (П). Партия bQ,wi,bi,b2,W2,... считается

выигрыннюй для игрока (I), если выполнены условия:

1. Для каждого г фигура —— является монотонным частным

случаем одного из правил вывода исчисления

2. Кратность размеченных формул в антецеденте начальной се квенции и антецедентах всех секвенций, предлагаемых игроком

(I), равна единице. 3. Последний ход в игре является ходом игрока (II) и состоит в

выборе одной из аксиом исчисления RCLTQ. Количество ходов в игре и размер каждого хода, согласно лемме

3.4.2, полиномиально ограничены, а предикат выигрыша игрока (I)

вычислим за полиномиальное время. Из известной игровой характе ризации класса PSPACE (см. [10], [8]) следует, что для каждой такой

игры множество

Ji4 = {^ 0 I игрок (I) обладает выигрышной стратегией

в игре с начальной конфигурацией Ьо }

принадлежит классу PSPACE. Условие принадлежности множеству Л4 начальной конфигурации

Г => F эквивалентно выводимости в RCLTQ ЭТОЙ секвенции посред ством монотонного вывода без новторяющихся формул в антецеден тах. Поэтому лемма 3.3.3 устанавливает полиномиальную сводимость

множества всех выводимых в RCLTG секвенций к Л4. Это означа ет принадлежность множества всех выводимых в RCLTG секвенций

классу PSPACE.С л е д с т в и е 3.4.4 Проблема выводимости из гипотез в исчислении

RCI > лесисит в классе PSPACE. Доказательство. В доказательстве теоремы 3.3.6 ностроено ноли номиально ограниченное по времени сведение рассматриваемой за дачи к задаче выводимости секвенций в исчислении RCLTG. Теорема 3.4.5 Проблемы выводимости секвенций для исчисления

RCLTG и выводимости формул для исчисления RCI > являются

PSPACE-полными. Доказательство. Верхняя оценка сложности {PSPACE) для этих

двух задач установлена в теореме 3.4.3 и следствии 3.4.4 соответ ственно. Нижняя оценка {PSPACE-труддостъ) следует из извест ного результата Р. Статмана (см. [18]), установившего PSPACE-

полноту имнликативного фрагмента интуционистской логики выска зываний INT_>, т.е. множества всех имнликативных формул, являю щихся теоремами интуиционистской логики высказываний INT. Секвенциальная формулировка исчисления INT_+ состоит из всех

аксиом исчисления RCLTG, не содержащих термов, и нравил (Ь^),

(Я-*) и (L С). Поэтому все секвенции, выводимые в INT_ ,^ выводи мы также и в исчислении RCLTG. Из факта устранимости сечения в

RCLTG (теорема 3.2.5) следует, что обратное также верно. Кроме то го, каждая не содержащая термов формула F языка RCI > нравильно

построена и F^ = F, откуда RCL_^ \- F ^ RCLTG Ь {=^ F) но тео реме 3.1.4. Таким образом, для имнликативных пропозициональных

формул F справедливо

InthF ^ RCLTG h(=^F) ^ RCL_ h F.Это сведение переносит нижнюю оценку для INT_^ {PSРАСЕ трудность) на проблемы выводимости для исчислений RCLTG И

Таким образом, задача раснознавания выводимости формул из

гипотез для рефлексивной комбинаторной логики PSРАСE-пoлпгi,

причем нижняя оценка достигается уже в случае пустого множества

гинотез. Для сравнения оценим сложность отраженного фрагмента

рефлексивной комбинаторной логики, т.е. множества выводимых в

RCI > формул вида t:F. Лемма 3.4.6 RCI > h t:F тогда и только тогда, когда формула t:F

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

подтермов. Доказательство. Пусть RCI > h t:F. По онределению выводимо сти в RCI >, формула t:F правильно построена. Тогда определена

размеченная формула {t:FY = {ty-.F^ и секвенция =^ {tY'.F^ выводи ма в исчислении RCLTG С ПОМОЩЬЮ правильно построенного вывода,

не использующего правило сечения (теоремы 3.1.4, 3.2.5). Индукци ей по длине такого вывода покажем, что размеченный терм {ty не

содержит размеченных подтермов-переменных. Последним правилом в выводе может быть только одно из правил

{R г), {R !) или {R •). В случае правила {Я г) единственным разме ченным нодтермом терма {ty = г^'^ является он сам. При этом г есть

идентификатор одной из констант, ноэтому {ty не является перемен ной. В случаях правил (Я !) и {Я •) утверждение непосредственно

следует из индуктивного предположения. При переводе (•)'' подтермы-переменные переходят в размеченные

подтермы-переменные, ноэтому у терма t нодтермов-переменных нет.Предположим теперь, что формула t: F правильно построена и

терм t не имеет подтермов-переменных. Тогда размеченная формула

{t: Fy =• {ty: F^ определена и является типом, причем размечен ный терм {ty не содержит размеченных подтермов-переменных. Ин дукцией по выводу в исчислении RCLT-wf суждения "(i:F)' ' - тип"

покажем, что секвенция => {t: Fy выводима в исчислении RCLTG

без правила сечения. Такой вывод будет правильно построенным по

лемме 3.1.3, откуда RCI > h t:F согласно теореме 3.1.4. Последним правилом в выводе суждения ^^{t:Fy - тип" может

быть только одно из правил 4 - 1 0 исчислепия RCLT-wf. В случае

правил 4, 5, 6, 8, 10 терм {ty оказывается константой и секвенцию

=^ {t:Fy удается вывести в RCLTG ПО правилу (Л г). Для правил 7

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

построения выводов секвенций, соответствующих посылкам, и про должить эти выводы применением одного из правил {R •) или (Я !). в качестве следствия получим следующую оценку. Теорема 3.4.7 Задача распознавания выводимости формул вида

tiF в исчислении RCI > разрешима за полиномиальное время (от

размера формулы). Доказательство. Лемма 3.4.6 за полиномиальное время сводит за дачу распознавание выводимости формулы t:F к проверке ее пра вильной построенности. Последняя разрешима за полиномиальное

время согласно теореме 2.5.5.

1. S. Artemov. Operational Modal Logic. Technical Report MS1.95-29, Cornell University, 1995.

2. S. Artemov. Logic of proofs: a unified semantics for modality and A-terms. Technical Report CFIS 98-06, Cornell University, 1998

3. S. Artemov. Explicit provability and constructive semantics. The Bulletin of Symbolic Logic, 7(l):l-36, 2001.

4. S. Artemov. Unified semantics for modality and lambda-terms via proof polynomials. In: Kees Vermeulen and Ann Copestake eds., Algebras, Diagrams and Decisions in Language, Logic and Computation, CSLI Publications, Stanford University, 2002.

5. С. Артемов. Подход Колмогорова и Геделя к интуиционистской логике и работы последнего десятилетия в этом направлении. Успехи матем. наук, 2004, 59, вып. 2 (356), 9-36.

6. S.Artemov, L.Beklemishev. Provability logic. In D.Gabbay, F.Guenthner, eds., Handbook of Philosophical Logic, 2nd ed., v. 13, 229-403, Kluwer, Dordrecht, 2004.

7. M. Bidoit, J. Corbin. A Rehabilitation of Robinson's Unification Algorithm. Information Processing, 83:909-914, 1983.

8. A.K. Chandra, D.C. Kozen, L.J. Stockmeyer. Alternation. J. Assoc. Comput. Mach., v. 28, 1981, pp 114-133.

9. R.L. Constable. Types in logic, mathematics and programming. In S.R. Buss, ed., Handbook of proof theory, chapter X, Elsevier Science B.V., 1998, pp. 684-786.

10. А. Китаев, А. Шень, M. Вялый. Классические и квантовые вычисления. М.: МЦНМО, ЧеРо, 1999.

11. С.К. Клини. Введение в метаматематику. М.: ИЛ, 1957.

12. R. Kuznets. On the complexity of explicit modal logics. In Computer Science Logic 2000, volume 1862 of Lecture Notes in Computer Science, pages 371-383. Springer-Verlag, 2000.

13. R. Ladner. The computational complexity of provability in systems of modal logic. SIAM Journal of Computing, v.6 (3), 1977, pp. 467480.

14. P. Martin-Lof. An intuitionistic theory of types. In G. Sambin, J. Smith, eds., Twenty five years of Constructive Type Theory, Oxford Logic Guides, v. 36, 1998, pp. 127-172.

15. Э. Мендельсон. Введение в математическую логику. М.: Наука, 1976.

16. A. Mkrtychev. Models for the logic of proofs. Lecture Notes in Computer Science, v. 1234, 266-275. Springer, 1997.

17. J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, v. 12, n. 1, 1965, pp. 23-41.

18. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Comput. Sci. 9, 1979, pp. 67-72

19. A. S. Troelstra, H. Schwichtenberg. Basic proof theory. Cambridge: Cambridge Univ. Press, 1996.Работы автора по теме диссертации

20. Н.В. Крупский. О сложности фрагментов логики доказательств. В сб.: Труды XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В. Ломоносова, 2002, 96-98.

21. N. Krupski. On the complexity of the reflected logic of proofs. CUNY Ph.D Program in CS Technical Reports, TR-2003007, 2003, 12 p. http://www.es.gc.cuny.edu/tr/techreport.php?id=81

22. Н.В. Крупский. О синтаксисе рефлексивной комбинаторной логики. Деп. в ВИНИТИ, №412-В2005, М. ВИНИТИ, 2005, 29 с.

23. N. Krupski. Typing in Reflective Combinatory Logic. CUNY Ph.D Program in CS Technical Reports, TR-2005013, 2005, 24 p. http://www.es.gc.cuny.edu/tr/techreport.php?id=166

24. Н.В. Крупский. Минимальные модели и сложность фрагментов логики доказательств. Вестник МГУ, сер. 1., Математика, Механика, 2006, №1. 52-53.