Введение к работе
Актуальность темы. Идея изучения доказуемости сред-
гвами модальной логики была впервые сформулирована К. Геделем [1]. Он предложил понимать модальную формулу ПЛ как утвержде-ие о доказуемости А. В качестве логики, аксиоматизирующей есте-гвенные свойства доказуемости, Гедель сформулировал систему 54.
При дальнейшем уточнении доказуеиостной семантики для мо-алыюсти было предложено считать, что выражает выводимость некоторой формальной системе, например в арифметике Пеано РА. огда естественным образом возникает определение доказуемост-М1 интерпретации модального языка в арифметический, при ко-эрой оператору D соответствует стандартная геделевская формула сказуемости Provable(-). Логика 54 оказалась некорректной отно-ітельно такой интерпретации. В [2] Р. Соловеем было показано, го множество формул, выводимых в РА при любой интерпретации, звпадает с логикой Геделя-Леба GL, а также построена логика 5, ароматизирующая модальные принципы, истинные в стандартной одели арифметики.
Логики формальной доказуемости Соловея оказались несовместными с логикой Геделя 54. Причина этого кроется в искажении зойств доказуемости, возникающем на этапе арифметического ко-ировання и связанном с некатегоричностью формальной арнфме-нки. А именно: арифметическое предложение Pwvable(\ip]) оэна-ает "существует доказательство х формулы ф", и это х может ока-іться нестандартным числом. Поэтому Provablt(\ip\) слабее нефор-ального утверждения о доказуемости ф.
Новый подход, предложенный С. Н. Артемовым в [3], состоял в ом чтобы сделать объектом изучения предикат доказательств "р сть доказательство теоремы F". Для этого пропозициональный зык был расширен переменными по доказательствам рі. В артритической интерпретации этим переменным соответствуют нату-
'Godel К. Eine Interpretation ties intuitionistischen Aussagenkalkuls j Ergebnisse Math. Colloq. — 1933. — pd. 4, P. 39-40.
2Solovay R.M. Provability interpretation of modal logic // Israel Jour-al of Mathematics. — 1976. — Vol. 25. — P. 287-304.
3Artemov S., Stra/3en T. The Basic Logic of Proofs // Lect. Notes in Ътр. Sci. — 1993. — Vol. 702. — P. 14-28.
ральные числа — коды индивидуальных доказательств. Формулы
представляющие отношение ир есть доказательство формулы F"
образуются при помощи оператора доказательств [)() согласш
правилу: если F — формула up — переменная по доказательствам
то [p]F — формула. В [3] были построены разрешимые арнфме
тическн полные системы, аксиоматизирующие свойства различны}
классов предикатов доказательств (т.е. фактически классов эффек
тивных кодировок выводов в РА). В работе [4] минимальны!*:
язык логики доказательств был расширен оператором доказуемости и сформулированы системы В, J7, М, Вы, F* и Мы, которые дают совместное описание свойств формальной доказуемости и предикатов доказательств. Логики В, J- и Лі аксиоматизируют соответственно свойства произвольных предикатов доказательств, функциональных предикатов и стандартного геделевского предиката, которые можно обосновать средствами РА. Логики В", Ти и Мш формализуют принципы, истинные в стандартной модели при интерпретациях, основанных на предикатах доказательств соответствующих классов.
Динамическая логика доказательств СР была введена в [5]. В ней квантор существования по доказательствам, содержащийся в D, заменяется на явный терм, содержащий полную информацию о доказательстве. Такие термы строятся из переменных по доказательствам при помощи функциональных символов (двуместные х, + и одноместный !), представляющих рекурсивные операции над доказательствами. Эти операции описываются следующими условиями:
Opl [t](A -* В) -» ([s\A ->{tx s]B)
Ор2 \І\А -> \\t\[i\A
ОрЗ [t)A -> [t + s]At ls]A ->{t + a]A.
Система СР, построенная в [5], обладает следующими свойствами:
Арифметическая полнота. СР аксиоматизирует множество формул, доказуемых в РА (истинных в стандартной модели) при всех арифметических интерпретациях, основанных на нормальных
4Artemov S. Logic of Proofs // Annals of Pure und Applied Logic. — 1994. — Vol. 67. -- P. 29 59.
5 Artemov S. Operational modal logic: Techii. Rep. No 95 29. — Mathematical Science Institute, Cornell University, 1995.
недетерминированных предикатах доказательств (т.е., неформально говоря, таких, для которых могут быть определены рекурсивные операции, реализующие х, -f и !).
Рункциональная полнота. Динамическая логика доказательств реализует в виде 7'-термов все операции над доказательствами, допускающие пропозициональное описание в арифметике.
Реализация 54. Модальным аналогом динамической логики доказательств при Р-переводе, состоящем в замене всех вхождений ft] на , является 54. Перевод всякой Р-теоремы доказуем в 54, и обратно, всякая формула, выводимая в 54, является О-переводом некоторой теоремы СР.
Цель работы. Построить и изучить динамическую логику оказательств, дающую совместное описание формальной доказуе-;ости и вычислимых операций над доказательствами, допускающих ропоэицнональное описание.
Исследовать возможность эффективного описання свойств предн-атов доказательств в языке первого порядка с оператором доказа-ельств.
Методы исследования. В диссертации использованы методы остроешш канонической модели и погружения ее в арифметику, совершенствованные автором, а также стандартная техника полу-ения нижних оценок сложности предикатных логик, соответствую-щх арифметическим теориям, основанная на теореме Тенненбаума единственности рекурсивной модели формальной арифметики.
Научная новизна работы. Все результаты диссертации является новыми.
Найдена естественная аксиоматизация динамической логики до-азательств с оператором формальной доказуемости. Полученная нстема М.СР включает в себя как логику доказуемости Соловея IL, так и динамическую логику Артемова СР. Налігше модалыю-гп в языке позволило ввести две новые элементарные операции ад доказательствами. Установлена разрешимость, арифметическая функциональная полнота конечных расширений базисного фраг-кшта системы М.СР.
Дано определение сильного и слабого варианта интерполяцион-ого свойства Крейга для логик доказательств. Описаны логики оказательств, обладающие интерполяционным свойством.
Получены нижние оценки сложности предикатной логики доказа тельств, показывающие невозможность эффективного описания своіі предикатов доказательств в языке первого порядка.
Теоретическая и практическая ценность. Работа носиі теоретический характер. Ее методы и результаты могут быть по лезны специалистам в области логик доказуемости и теоретическої информатики.
Апробация работы. Основные результаты, полученные і диссертации, докладывались на семинаре "Теория доказательств' (руководители семинара — профессор С. Н. Артемов и к.ф.-м.н Л. Д. Беклемишев), на семинаре лаборатории математической логнкі ПОМИ и на международных конференциях "Логические основанш информатики" LFCS'94 (г. Санкт-Петербург), LFCS'97 (г. Ярославлі н 10 Международном конгрессе по логике, методологии и фплософш науки (Флоренция, 1995).
Публикации. Результаты диссертации опубликованы в четы рех работах автора, перечисленных в конце автореферата.
Структура и объем работы. Диссертация состоит из вве дения и трех глав, разбитых на десять параграфов. Список лите ратуры содержит 21 наименование. Общин объем диссертации 7' страниц.