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

Московский государственный университет имени М. В. Ломоносова

На правах рукописи

0050471ЛI

Дашков Евгений Владимирович

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

01.01.00 - математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

2 0 СЕН 2012

Москва - 2012

005047017

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

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

Беклемишев Лев Дмитриевич член-корреспондент РАН Артёмов Сергей Николаевич доктор физико-математических наук, профессор, The Graduate Center of the City University of New York, США, Distinguished Professor Шапировский Илья Борисович кандидат физико-математических паук, Институт проблем передачи информации имени A.A. Харкевича РАН, старший научный сотрудник Институт математики имени С. Л. Соболева Сибирского отделения РАН Защита состоится 28 сентября 2012 г. в 16 часов 45 минут на заседании диссертационного совета Д 501.001.84 при Московском государственном университете имени М. В. Ломоносова по адресу: РФ, 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ, Механико-математический факультет, аудитория 14-08.

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

Автореферат разослан 28 августа 2012 г.

Ученый секретарь диссертационного совета Д 501.001.84 при МГУ д.ф-м.н., профессор f ff , Иванов А. О.

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

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

Актуальность работы. Первая глава диссертации посвящена рассмотрению интуиционистской логики доказательств iLP. Логика доказательств LP1 введена С. Н. Артёмовым и в настоящее время активно исследуется. LP является расширением исчисления высказываний в языке, представляющем доказательства как формальные объекты. Термы, выражающие доказательства. строятся из констант и переменных с помощью операций, соответствующих естественным операциям над выводами. Получаемые формулы вида t: F предполагают толкование <t есть доказательство F». Логика LP полна относительно арифметики Пеано РА при интерпретации t: F арифметической формулой «Г есть вывод F* в арифметике Пеано».

Интуиционистская арифметика НА —наиболее известная теория, формализующая понятие конструктивного доказательства. В силу известных теорем Р. Соловея,2 логикой доказуемости классической арифметики РА является логика Геделя-Лёба GL. Вопрос о логике доказуемости теории НА, впервые поставленный А. Виссером,3 длительное время остается открытым.4 Кроме того, — в частности, в связи с последним вопросом — представляет интерес отыскание логики доказательств теории НА. Так, подходящим образом определенная интуиционистская логика доказательств позволяет выра-

' Artcmov S. Explicit provability and constructive semantics // The Bulletin for Symbolic Logic. — 2001. — Vol. 7, no. 1. - P. 1-30.

2 Solovay R. Provability interpretation of modal logic // Israel Journal of Mathematics. — 197G. — Vol. 25, no. 3-4. - P. 237-304.

3 Visser A. Aspects of diagoualization and provability : PhD. thesis / A. VLsser ; Department of Philosophy, Utrecht University. - 1081.

4 Bekleniishev L„ Visser A. Problems in the Logic of Provability /,/ Mathematical Problems from Applied Logic I: Logics for the XXlst Century / Ed. by D.M. Gabbay, S.S. Goncharov, M. Zakharyashev. - International Mathematical Series: vol. 4. Springer, 200G.

зить допустимые в НА пропозициональные правила.5 которые, вследствие интуиционистского характера этой теории, не являются непременно выводимыми.

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

Проблема построения арифметически полной интуиционистской логики доказательств рассматривалась С. Н. Артёмовым и Р. Имхофф.7 В указанной работе ими вводится базовая интуиционистская логика доказательств iBLP и интуиционистская логика доказательств iLP. В отличие от iLP, логика iBLP не содержит операций над термами, представляющими доказательства. Там же определена естественная арифметическая интерпретация логики iBLP в НА и доказаны корректность и полнота iBLP относительно этой интерпретации, а также выдвинута гипотеза полноты iLP относительно надлежащей интерпретации в НА. Мы доказываем эту гипотезу.

Кроме того, в настоящей диссертации предложена семантика Крипке для логик iBLP и iLP. развивающая подход А. Мкртычева8 и М. Фиттинга9 к

5 IemhofT R. Provability logic and admissible rules : PhD thesis / R. IemhofT ; University of Amsterdam. — 2001.

6 Artcmov S. Unified semantics for modality and Л-terms via proof polynomials // Algebras, Diagrams and Decisions in Language. Logic and Computation / Ed. by K. Vermculen, A. Copcstakc. — Stanford University. 2002.

7 Artemov S., Iemhoff R. The basic intuitionistic logic of proofs /'/ The Journal of Symbolic Logic. — 2007. — Vol. 72, no. 2. - P. 439-451.

8 Mkrtychev A. Models for the logic of proofs // Logical Foundations of Computer Science, 4th International Symposium LFCS'97 / Ed. by S.I. Adiati, A. Nerode. — Lecture Notes in Computer Science 1234. — 1997. — P. 266-275.

9 Fitting M. The logic of proofs, semantically // Annals of Pure and Applied Logic. — 2005. — Vol. 132,

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

Во второй главе диссертации рассматривается фрагмент полимодальной логики доказуемости GLP в некотором обедненном языке. Интерес к логике GLP и этому ее фрагменту вызван, прежде всего, приложениями к теории доказательств.

Л. Д. Беклемишев предложил10 новый подход к ординальному анализу арифметических теорий, основанный па понятии градуированной алгебры доказуемости, т.е. алгебры Линденбаума рассматриваемой теории, обогащенной операторами доказуемости (или непротиворечивости). Пусть СТ означает алгебру Линденбаума теории Т. Предполагая Т достаточно сильной, введем операторы на Ст:

(п)т: [F] ^ [n-Conr(F)],

где [F] означает класс эквивалентности формулы F, а формула n-Conr(F) естественным образом выражает совместность множества всех истинных П„-прсдложсний и формулы F в теории Т. Тогда градуированной алгеброй доказуемости теории Т называется структура Мт = (£т,{(п)т \ п < w}). Термы Мт можно отождествить с формулами некоторого модального языка.

Действительно, рассмотрим язык £ с пропозициональными переменными, связками 1, Т, A, V. -> и (п) для всех п < и>. При этом считаем -ip, V? О ф и [п}(р -i(n)-itp сокращениями.

Для всякой (достаточно сильной) корректной теории Т логикой алгебры Мт является система GLP, введенная Г. К. Джапаридзе11 в 1986 г. (см. тж.

no. 1. - Р. 1-25.

10 Beklemishev L. Provability algebras and proof-theoretic ordinals, I // Annals of Pure and Applied Logic. — 2004. - Vol. 128. - P. 103-123.

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

в изложении К. Н. Игнатьева12). Г. К. Джапаридзе фактически доказал, что для любой формулы языка £ выполнено

Мт 1= (<р(х) = Т) «Ф- GLP h р(х).

С применением логики GLP была получена система ординальных обозначений до ординала со, ординальный анализ арифметики Пеано РА и ряда ее фрагментов,10 а также был построен новый пример комбинаторного утверждения, независимого от РА.13 В действительности, как заметил JI. Д. Беклемишев, для получения этих результатов достаточно рассматривать позитивный фрагмент GLP+ логики GLP, т.е. множество доказуемых в GLP эк-вивалентностей формул позитивного* полимодального языка £ + с пропозициональными переменными, Т, Л и модальными связками (п) для всех п < си. Более того, упомянутая система ординальных обозначений строится из позитивных формул без переменных. Таким образом возможно упростить доказательства указанных результатов.

Задача аксиоматизации позитивного фрагмента GLP+, сформулированная Л. Д. Беклемишевым и А. Висссром,4 решена в настоящей диссертации.

Заметим, что позитивный формализм допускает более широкий класс арифметических интерпретаций — в соответствие переменным могут быть поставлены теории (т. е. фильтры в Мт), а не только отдельные предложения. Это обстоятельство способствует анализу более сильных, чем арифметика Пеано, теорий методом градуированных алгебр доказуемости.

' В литературе по модальным логикам принято более широкое понимание позитивного языка: обычно позитивным считается язык определяемый ниже.

12 Ignaticv К. On strong provability predicates and the associated modal logics // The Journal of Symbolic Logic. - 1031. - Vol. 53. no. 1. - P. 2-19-290.

13 Deklemishev L. The worm principle // Logic Colloquium '02 / Ed. by Z. Chatzidakis, P. Koepke. W. Pohlers. - Lecture Notes in Logic 27. — AK Peters, 2006. — P. 75-95.

И. Б. Шапировский показа'!,14 что проблема выводимости в логике GLP является PSPACE-иолной. Мы доказываем, что фрагмент GLP+ разрешим за полиномиальное время. Таким образом, позитивный формализм проще не только синтаксически, но и алгоритмически.

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

Позитивные в некотором более широком смысле модальные логики рассматривались ранее. Дж. Данн15 исследовал минимальную нормальную модальную логику К}/1 в языке £D со связками A, V, □, О, Т, ±, а также некоторые ее расширения. Аксиомами и теоремами при этом считаются утверждения вида <р h ф. С помощью обычной семантики Крипке Данн установил, что К консервативна над К^1, или, другими словами, К}1 аксиоматизирует фрагмент логики К в языке £D:

10 ЬКТ! ф & Ьк <р -> ф,

для любых <р, ф G £d. Однако, в смысле предложенной семантики некоторые расширения Kjx оказались неполными: например, в каждой шкале, где истинна Пу h ПП\р, истинной оказывается и 00<¿> H 0V-, притом что второе утверждение не выводится из первого в К^-1. Эта трудность была разрешена С. Чслани и Р. Жансана,16 доказавшими полноту ряда расширений К^1 относительно шкал, где отношение достижимости согласовано с некоторым пред-порядком так, что допускаются лишь замкнутые вверх относительно предпо-рядка оценки переменных.

14 Shapirovsky I. PSPACE-decidability of Japaridze?s polymodal logic // Advances in Modal Logic / Ed. by C. Areces. R. Coldblatt. — Vol. 7. - College Publications, 2008. — P. 289-301.

15 Dunn J. Positive modal logic // Studia Lógica. - 1995. - Vol. 55, no. 2. - P. 301-317.

16 Celani S., Jansana R. A new semantics for positive modal logic // Notre Dame Journal of Formal Logic. -1997. - Vol. 38, no. 1. - P. 1-18.

Упомянутые результаты15,16 позволяют получить аксиоматизацию позитивных фрагментов многих хорошо известных логик, являющихся расширениями К посредством принципов вида tp —* ф, где ¡р, ф € Си- Таковы В, Т, D, S4, S5 и др. Однако, например, к логике Геделя-Лёба GL = К 4 + О<р —> ()(pA-i()tp) эти результаты непосредственно не применимы. Из результатов настоящей работы следует совпадение £+-фрагментов логик GL и К4, однако легко убедиться, что K4d GLd-

Вопросы сложности модальных логик в обедненных языках рассматривались ранее преимущественно в контексте дескрипционных логик. В дескрип-

17 lg on

цноннои постановке исследовалась1''10'13'^ сложность задачи, представимои в модальных терминах следующим образом. Пусть формулы построены из переменных, связок Т, _L, Л и не более чем счетного множества связок 0Г-Проверить: «для всякой модели из данного класса, если во всех точках модели выполнено некоторое конечное множество импликаций ipi ф^ то во всех точках этой модели выполнена '-р -> фУстановлена PTIME-разрешимость этой задачи для класса всех шкал Крипке и получены оценки сложности для некоторых классов шкал. Тем не менее, из известных нам результатов в этой области оценка сложности GLP+ очевидным образом не извлекается. Целью диссертационной работы является следующее: 1. Доказать гипотезу Артёмова-Имхофф7 о полноте интуиционистской логики доказательств iLP относительно естественной арифметической се-

17 Ba-ulcr F., Brandt S.: Lutz С. Pushing the EL envelope // IJCAI / Ed. by L.P. Kaelbling, A. Saffiotti. -2005. - P. 364-369.

18 Baadcr F., Brandt S., Lutz C. Pushing the EL envelope further // Proc. of OWLED / Ed. by K. Clark. P.F. Patcl-Schneider. - 2008.

19 Kurucz A.. Wolter F., Zakharyaschev M. Islands of tractability for relational constraints: towards dichotomy results for the description logic EL ,// Advances in Modal Logic / Ed. by L. Beklemishev, V. Goranko, V. Shehtman. - Vol. 8. - College Publications, 2010. - P. 271-291.

20 Sofronie-Stokkermans V. Locality and subsumption testing in EL and some of its extensions / / Advances in Modal Logic / Ed. by C. Areces. R. Goldblatt. - Vol. 7. - College Publications, 2008. - P. 315-330.

мантики.

2. Получить аксиоматизацию позитивного фрагмента логики GLP.

3. Исследовать вычислительную сложность проблемы выводимости для этого фрагмента.

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

1. Установлена полнота интуиционистской логики доказательств iLP относительно естественной арифметической семантики.

2. Дана аксиоматизация позитивных фрагментов логик GL и GLP как исчислений равенств.

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

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

Апробация работы. Результаты диссертации докладывались:

• На семинарах «Алгоритмические вопросы алгебры и логики» и «Логические проблемы информатики» кафедры математической логики и теории алгоритмов МГУ (неоднократно) в 2006-2012 гг.

• На международной конференции «Logical Models of Reasoning and Computation» (Москва, 2008).

• На международной конференции «Advances in Modal Logic» (Москва, 2010).

• На международном семинаре «Proof. Computation, Complexity» (Берн, 2010).

Публикации. Основные результаты диссертации опубликованы в трех печатных работах автора [ 1—3J, список которых приведен в конце автореферата.

7

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

Структура и объем диссертации. Диссертация состоит из введения, двух глав и библиографии. Общий объем диссертации составляет 80 страниц. Библиография включает 34 наименования.

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

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

В первой главе диссертации рассматривается интуиционистская логика доказательств ¡ЬР.

Определение 1. Формулы и термы языка определяются индуктивно следующим образом. Пусть Р и С суть формулы, ам1( термы. Тогда

• ±,р1,Ь: Г, FVG, /^АС, F -» б" суть формулы, гдep¿ пропозициональные переменные;

• с*, и,-,! t, fI• £ ■ в, 4 + я суть термы, где С; и и; доказательственные константы и переменные соответственно, а ^ для всех натуральных г — специальные знаки операций над термами.

Определение 2. Для языка, содержащего булевы связки, и произвольного п € и> обозначим через Уп множество примеров схемы

Д (Я-» СО-> Д.+1 V/Ъ+г 1=1_

п+2 п

Определение 3. Логика доказательств ¡ЬР в языке -С^р определяется следующими схемами аксиом и правилами вывода:

А1 Схемы аксиом интуиционистской пропозициональной логики

А2 —> /-1 (рефлексия)

АЗ Ь-.РУЫ-.Р

А4 -> й) (¿: Р -> й • Ь'.в) (аппликация)

А5 Ь: Г —! й: : (проверка доказательств)

АО s:FVí:F—>'S-fí:F (объединение доказательств) А7П если - 6 Уп

Сг

Л —> /?, Л

Ml -—--(modus ponens)

CS —ссли Л— аксиома iLP с: Л

и с —доказательственная константа. (свидетельства аксиом)

Определение 4. Будем рассматривать модели Кринке (IV. =$,11-), где ^ отношение частичного порядка и (х 1Ь р к х -4 у) => у 1Ь р. Вынуждение пропозициональных формул определим так, как для случая иптуиционистской пропозициональной логики. Модель называется моделью Имхофф, если:

1. шкалы всех конусов модели конечны;

2. всякое конечное подмножество II элементов модели имеет тесную нижнюю грань, т.е. для каждого II модель содержит такой элемент хо, что Хо ^ х для всех х € и, и ссли Хо -< у, то существует элемент х' 6 С/, удовлетворяющий условию х' у.

Определение 5. Пусть задана модель Имхофф К1 и свидетельская функция £: Тт£|1Р 2 ,1-р, где Тт/;1Р обозначает множество термов по определению удовлетворяющая условиям:

• если F G 6 £ (s) и F 6 £ (i), то С e £ (,s • f);

• если Fe£(i);Toi:Fe£(!t);

• если F e £ (i), то ^ e £ (s + i) П £ (t + s);

F

• если ^ € £ (t) и — € V„, то G € £ (fn t);

(jr

• если с—доказательственная константа, а Л —аксиома iLP, то А € £(с).

Тогда KlLP = (К1, £) можно рассмотреть как модель языка £,lp:

KiLP, x\ht:F^ KiLP lh F и F в £ (t).

Теорема 1. Логика iLP корректна и полна относительно моделей вида KiLP.

Семантика для логики iLP получается комбинацией данной Имхофф21 семантической характеристики допустимых правил вывода интуиционистской пропозициональной логики с подходом Мкртычева8 и Фиттинга9 к построению моделей логики доказательств. Также используется техника проективных формул, развитая Гилярди.22

Определение 6. Предикат доказательств — это примитивно рекурсивная арифметическая формула Prf(a;, у), такая что при всех (р 6 где -С^л

означает множество арифметических предложений. ЬПА <р имеет место тогда и только тогда, когда найдется число п € w, для которого N |= Prf (к,

Предикат доказательств Prf (х, у) назовем нормальным., если выполнены следующие условия:

21 IcmhofT R. Oil the admissible rules of intuitionistic propositional logic // The .Journal of Symbolic Logic. — 2001. - Vol. 66, no. 1. - P. 281-294.

22 Ghilardi S. Unification in intuitionistic logic // The Journal of Symbolic Logic. — 1999. - Vol. 64, no. 2. — P. 859-880.

• для всякого к 6 и! множество Т (к) {I | N Prf (А:. /)} конечно, причем функция к г{/ | I е Т (к)}п рекурсивная тотальная;

• для всяких к,1 € и существует п 6 и, такое что Т (к) U Т (I) С Т (п).

Определение 7. Пусть дан нормальный предикат доказательств Prf (х, у), а также рекурсивные тотальные функции ш, а, с и /„ для всех п € ы, такие что для любых ip, ф S и любых к, I, € и в N выполнено:

Prf (fc, >> -> (prf г^п) prf (ш

Prf (it, г^-i) V Prf (/,■>-■) Prf (а(Ы),гуЯ); Prf (/с, г^-i) Prf (с (к), rPrf(£, г^)"1);

Prf (Ä, г^п) Prf (д rpi)t если ^ e Vn.

ф

Тогда арифметическая интерпретация языка ¿¡lp есть произвольное отображение (•)*: £jlp U Tm£iLp -4 /Cj[A Uuj, удовлетворяющее условиям:

• JL* = _L; (•)* коммутирует с пропозициональными связками;

. (5 • ty = т (а*, ¿*); (s + t)'= а (.s\ Г); (! «)* = с (i*); (f„ t)* = In (f) для всех п € ш;

• (¿:F)* = Prf (i*, ^F*^).

Теорема 2. Пусть множество Ги {Л} С ¿¡lp конечно. Если r.FiLp Л, то существует арифметическая интерпретация (■)*, такая что 1 гНА А .

Полнота логики iLP относительно арифметической семантики устанавливается модификацией общей схемы доказательства полноты для логики доказательств LP, принадлежащей Артсмову,1 с применением техники проективных формул. Также использована теорема дс Йонга.23 Результаты первой главы, относящиеся к теореме 2, опубликованы в работе автора [3|.

23 Smorynski С. Applications of Kripke models // Mathematical Investigations of Intuitionistic Arithmetic and Analysis / Ed. by A. Troelstra. - Springer-VerlaR, 1973. - P. 324-391.

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

Определение 8. Полимодальный пропозициональный язык С имеет связки Т, -L, Л. V. —> и (п) для всех п € из. Позитивный язык £+ получается из L исключением всех связок, кроме Т, Л и (п) для всех п € из. Позитивный мономодальный язык £+(0) имеет связки Т, Л и О, причем последнюю мы отождествляем с (0) и считаем £+(0) С

Определение 9. Логика GLP задается в языке £ следующими схемами аксиом:

(i) Схемы аксиом пропозициональной логики; (и) -.<n)_L;

(ni) <n)(ip V ф) (п)<р V {п)ф;

(iv) (п)(р->{п)(<рЛ-<{п)<рУ,

(v) (п)(т)р —> (т)ф, если тп ^ п;

(vi) {n)-i(m)ip —> -i(m)y>, если m <п\ (v¡¡) (n)ip —> (m)ip, если m < n,

и правилами вывода: modus ponens и (Nec) h <p ф =>■ I- (n)y; (n)V'-

Определе1ше 10. Множество формальных равенств GLP+ ^ = ф \ GLP h <р о ^ и у?, ф € £+} называется позитивным фра?.мент,ом логики GLP. Задаваемое GLP+ отношение = на (£+)2 действительно является отношением эквивалентности.

Определение 11. Определим исчисление GLP® для равенств вида >.р = ф, где V?, ip 6 £+. Примем схему аксиом <р = tp и правила

12

'Р = Ф 1р — в в = Ф Ц> = Ф (р = Ф

ф = р р = ф (р А в = ф АО (п)р = (п)ф

для всех п < и. Пусть <р ^ ф означает р А ф = ¡р. Кроме указанных схем н правил, исчисление СЬР® задается схемами аксиом

1. Т Л р = р\

2. (р Аф)АО = рА(фАв);

3. р А ф = ф А <р\

4. р А р = р\

5. (п)(р А ф) ^ (п)'р А (п)ф\

0. (п){п)(р ^ {п)р\

7. (п)<р А {т)ф ^ {п)(<р А (т)ф), где т < щ

8. (п)(р ^ {т}р, где т < п.

Теорема 3. Пусть р,ф е £+. Тогда СЬР Н р гр равносильно СЬР® Ь •р = ф.

Определение 12. Шкала Крипке {IV. {/?п}п<=^) называется 7+-шкалой, если

1. Уж, у, г (хЯпу к. уИ^г хЯ„г)\

2. тп < П => Яп С Дт;

3. 1П < п => Ух, у (х1гпу => Уг (хЯтг => уЯтг)).

Вынуждение формул языка -С определяется обычным образом.

Теорема 4. Для любых -р,ф € £+ тогда и только тогда СЬР® Н <р ^ ф, когда в каэюдой (конечной) .1+-модели вынуждается р —> ф.

Определение 13. Исчисление К4® в языке £+(0) получается, если в определении GLP® ограничиться аксиомой и правилами для =, а также неравенствами (1-6), полагая всюду в последних п = 0.

Теорема 5. Пусть L есть произвольная моиомодальиая логика, промежуточная между К4 и GL. Тогда L I- ¡р о ф равносильно К4® I- ip = ф для всех (р,ф е £+(0).

Определите 14. Сложность \ip\ формулы (р е £+ есть ее длина как слова в алфавите {Т,ри ... ,рп,..., Л, (0),..., (п),...}.

Теорема 6. Проблема принадлежности к множеству GLP+ равенств вида ■р — ф разрешима за время, полиномиальное от N = \<р\ + \ф\.

Результаты об аксиоматизации и финитной аппроксимируемости получены стандартными методами. При этом используется сведение24 логики GLP к ее подсистеме J. полной по Крипке, и семантическая характеристика замкнутого фрагмента GLP.12 Полиномиальная разрешимость рассматриваемого фрагмента логики GLP устанавливается с применением полученной семантической характеристики. Результаты второй главы опубликованы в работе автора [1|.

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

21 Bcklcmishcv L. Kripkc semantics for provability logic GLP // Annals of Pure and Applied Logic. - 2010. -Vol. 161, no. 6. — P. 756-774.

Список публикаций

1. Дашков Е. В. О позитивном фрагменте полимодалыюй логики доказуемости // Математические заметки. - 2012. - Т. 91, № 3. - С. 331-346.

2. Dashkov Е. On positive fragments of polymodal provability logic // Proof, Computation, Complexity PCC 2010 International Workshop / Ed. by K. Brünnlcr, Т. Studer. — Institut für Informatik und angewandte Mathematik, University of Bern, 2010. - P. 13-15.

3. Dashkov E. Arithmetical completeness of the intuitionistic logic of proofs // Journal of Logic and Computation. — 2011. — Vol. 21, no. 4. - P. 665-682.

Подписано в печать 24.08.2012 Формат 60x88 1/16. Объем 1.0 п.л. Тираж 100 экз. Заказ № 1231 Отпечатано в ООО «Соцветие красок» 119991 г.Москва, Ленинские горы, д.1 Главное здание МГУ, к. А-102

Введение.

Глава 1. Интуиционистская логика доказательств.

1.1. Язык.

1.2. Логика іЬР.

1.3. Семантика Крипке.

1.4. Арифметическая семантика

Глава 2. Позитивный фрагмент полимодальной логики доказуемости

2.1. Позитивный фрагмент системы СЬР.

2.2. Семантика Крипке для СЬР+.

2.3. Случай одной модальности.

2.4. Сложность фрагмента ОЬР+

Первая глава диссертации посвящена рассмотрению интуиционистской логики доказательств ¡ЬР. Логика доказательств ЬР [4] введена С. Н. Артёмовны и в настоящее время активно исследуется. ЬР является расширением исчисления высказываний в языке, представляющем доказательства как формальные объекты. Термы, выражающие доказательства, строятся из констант и переменных с помощью операций, соответствующих естественным операциям над выводами. Получаемые формулы вида £: .Р предполагают толкование есть доказательство Логика ЬР полна относительно арифметики Пеано РА при интерпретации £: ^ арифметической формулой «£* есть вывод Р* в арифметике Пеано».

Интуиционистская арифметика НА —наиболее известная теория, формализующая понятие конструктивного доказательства. В силу известных теорем Р. Соловея [32], логикой доказуемости классической арифметики РА является логика Гёделя-Лёба СЬ. Вопрос о логике доказуемости теории НА, впервые поставленный А. Виссером [33], длительное время остается открытым [13]. Кроме того,— в частности, в связи с последним вопросом — представляет интерес отыскание логики доказательств теории НА. Так, подходящим образом определенная интуиционистская логика доказательств позволяет выразить допустимые в НА пропозициональные правила [22], которые, вследствие интуиционистского характера этой теории, не являются непременно выводимыми.

Ранее исследовалась [5] интуиционистская логика доказательств 1ЬР, определяемая как фрагмент ЬР с интуиционистскими пропозициональными аксиомами вместо классических. Однако, логика 1ЬР не полна относительно интуиционистской арифметики НА и, таким образом, не решает вопроса о логике доказательств этой теории.

Проблема построения арифметически полной интуиционистской логики доказательств рассматривалась С. Н. Артёмовым и Р. Имхофф [6]. В указанной работе ими вводится базовая интуиционистская логика доказательств 1ВЬР и интуиционистская логика доказательств ГЬР. В отличие от гЬР, логика 1ВЬР не содержит операций над термами, представляющими доказательства. Там же определена естественная арифметическая интерпретация логики 1ВЬР в НА и доказаны корректность и полнота ¡ВЬР относительно этой интерпретации, а также выдвинута гипотеза полноты ЛР относительно надлежащей интерпретации в НА. Мы доказываем эту гипотезу. Соответствующие результаты опубликованы в работе автора [17].

Кроме того, в настоящей диссертации предложена семантика Крипке для логик 1ВЪР и ЛР, развивающая подход А. Мкртычева [27] и М. Фиттин-га [19] к построению моделей логики доказательств. Доказаны соответствующие теоремы о полноте и корректности, а также получен ряд следствий из них.

Во второй главе диссертации рассматривается фрагмент полимодальной логики доказуемости СЬР в некотором обедненном языке. Интерес к логике СЬР и этому ее фрагменту вызван, прежде всего, приложениями к теории доказательств.

Л. Д. Беклемишев предложил [9] новый подход к ординальному анализу арифметических теорий, основанный на понятии градуированной алгебры доказуемости, т. е. алгебры Линденбаума рассматриваемой теории, обогащенной операторами доказуемости (или непротиворечивости). Пусть Ст означает алгебру Линденбаума теории Т. Предполагая Т достаточно сильной, введем операторы на Стп)т И [п-Сопг(^)], где [Р] означает класс эквивалентности формулы а формула п-Сопу(Р) естественным образом выражает совместность множества всех истинных Пп-предложений и формулы Г в теории Т. Тогда градуированной алгеброй доказуемости теории Т называется структура Л4т = {£тЛ{п)т | п < Термы Л4т можно отождествить с формулами некоторого модального языка.

Действительно, рассмотрим язык & с пропозициональными переменными, связками Т, А, V, —> и (п) для всех п < со. При этом считаем -чр, ф и [п)ср ^ (п)-чр сокращениями.

Для всякой (достаточно сильной) корректной теории Т логикой алгебры М-т является система СЬР, введенная Г. К. Джапаридзе [2] в 1986 г. (см. тж. в изложении К. Н. Игнатьева [23]). Г. К. Джапаридзе фактически доказал, что для любой формулы <р языка £ выполнено

Мт И Ух{<р{х) = Т) ^ СЬР Ь </?(£).

С применением логики СЬР была получена система ординальных обозначений до ординала £о, ординальный анализ арифметики Пеано РА и ряда ее фрагментов [9], а также был построен новый пример комбинаторного утверждения, независимого от РА [10]. В действительности, как заметил Л. Д. Беклемишев, для получения этих результатов достаточно рассматривать позитивный фрагмент СЬР+ логики СЬР, т.е. множество доказуемых в СЬР эквивалентностей формул позитивного* полимодального языка с пропозициональными переменными, Т, А и модальными связками (п) для всех п < и>. Более того, упомянутая система ординальных обозначений строится из позитивных формул без переменных. Таким образом возможно упростить доказательства указанных результатов. В литературе по модальным логикам принято более широкое понимание позитивного языка: обычно позитивным считается язык определяемый ниже.

Задача аксиоматизации позитивного фрагмента СЬР+, сформулированная Л. Д. Беклемишевым и А. Виссером [13], решена в настоящей диссертации.

Заметим, что позитивный формализм допускает более широкий класс арифметических интерпретаций — в соответствие переменным могут быть поставлены теории (т. е. фильтры в Л4т), а не только отдельные предложения. Это обстоятельство способствует анализу более сильных, чем арифметика Пеано, теорий методом градуированных алгебр доказуемости.

И. Б. Шапировский показал [28], что проблема выводимости в логике СЬР является РЗРАСЕ-полной. Мы доказываем, что фрагмент СЬР+ разрешим за полиномиальное время. Таким образом, позитивный формализм проще не только синтаксически, но и алгоритмически.

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

Позитивные в некотором более широком смысле модальные логики рассматривались ранее. Дж. Данн [18] исследовал минимальную нормальную модальную логику в языке со связками А, V, □, О, Т, ±, а также некоторые ее расширения. Аксиомами и теоремами при этом считаются утверждения вида <р Ь ф. С помощью обычной семантики Крипке Данн установил, что К консервативна над К+-1, или, другими словами, Кр- аксиоматизирует фрагмент логики К в языке у Ьктх ф Ьк (р ф, для любых (р,ф € £в- Однако, в смысле предложенной семантики некоторые расширения К^-1 оказались неполными: например, в каждой шкале, где истинна □<£> Ь □□у?, истинной оказывается и 00Ь~ 0у?, притом что второе утверждение не выводится из первого в К+1-. Эта трудность была разрешена С. Челани и Р. Жансана [15], доказавшими полноту ряда расширений К]}1 относительно шкал, где отношение достижимости согласовано с некоторым предпорядком так, что допускаются лишь замкнутые вверх относительно предпорядка оценки переменных.

Упомянутые результаты [15, 18] позволяют получить аксиоматизацию позитивных фрагментов многих хорошо известных логик, являющихся расширениями К посредством принципов вида (р —>• ф, где (р,ф 6 Таковы В,Т,В,84, Б5 и др. Однако, например, к логике Гёделя-Лёба СЬ = К 4 + 0<р —> 0(</? А -1<>ф) эти результаты непосредственно не применимы. Из результатов раздела 2.3 следует совпадение £+-фрагментов логик СЬ и К4, однако легко убедиться, что К4о С СЬв

Вопросы сложности модальных логик в обедненных языках рассматривались ранее преимущественно в контексте дескрипционных логик. В дескрип-ционной постановке исследовалась [7, 8, 26, 31] сложность задачи, представи-мой в модальных терминах следующим образом. Пусть формулы построены из переменных, связок Т, 1, Л и не более чем счетного множества связок Ог-Проверить: «для всякой модели из данного класса, если во всех точках модели выполнено некоторое конечное множество импликаций (Р1 Фг, то во всех точках этой модели выполнена <р ф->. Установлена РТШЕ-разрешимость этой задачи для класса всех шкал Крипке и получены оценки сложности для некоторых классов шкал. Тем не менее, из известных нам результатов в этой области оценка сложности СЬР+ очевидным образом не извлекается.

Приводимые во второй главе диссертации результаты опубликованы в статье автора [1].

Благодарности

Автор благодарен своему научному руководителю члену-корреспонденту РАН Льву Дмитриевичу Беклемишеву за постоянное внимание к этой работе и ценные советы. Автор также признателен доценту Татьяне Леонидовне Яворской и всем сотрудникам кафедры математической логики и теории алгоритмов МГУ.

1. Дашков Е. В. О позитивном фрагменте полимодальной логики доказуемости // Математические заметки. — 2012.— Т. 91, № 3.— С. 331-346.

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

3. Рыбаков В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики // Матем. сб.— 1985.— Т. 128(170), № 3(11). — С. 321-338.

4. Artemov S. Explicit provability and constructive semantics // The Bulletin for Symbolic Logic. 2001. - Vol. 7, no. 1. - P. 1-36.

5. Artemov S. Unified semantics for modality and A-terms via proof polynomials // Algebras, Diagrams and Decisions in Language, Logic and Computation / Ed. by K. Vermeulen, A. Copestake. — Stanford University, 2002.

6. Artemov S., Iemhoff R. The basic intuitionistic logic of proofs // The Journal of Symbolic Logic. 2007. - Vol. 72, no. 2. - P. 439-451.

7. Baader F., Brandt S., Lutz C. Pushing the EL envelope // IJCAI / Ed. by L.P. Kaelbling, A. Saffiotti. 2005. - P. 364-369.

8. Baader F., Brandt S., Lutz C. Pushing the EL envelope further // Proc. of OWLED / Ed. by K. Clark, P.F. Patel-Schneider. 2008.

9. Beklemishev L. Provability algebras and proof-theoretic ordinals, I // Annals of Pure and Applied Logic. 2004. - Vol. 128. - P. 103-123.

10. Beklemishev L. The worm principle // Logic Colloquium '02 / Ed. by Z. Chatzidakis, P. Koepke, W. Pohlers. — Lecture Notes in Logic 27. — AK Peters, 2006. P. 75-95.

11. Beklemishev L. Kripke semantics for provability logic GLP // Annals of Pure and Applied Logic. 2010. - Vol. 161, no. 6. - P. 756-774.

12. Beklemishev L., Joosten J., Vervoort M. A finitary treatment of the closed fragment of Japaridze's provability logic // Journal of Logic and Computation. 2005. - Vol. 15, no. 4. - P. 447-463.

13. Boolos G., Burgess J., Jeffrey R. Computability and Logic.— Cambridge University Press, 2002.

14. Celani S., Jansana R. A new semantics for positive modal logic // Notre Dame Journal of Formal Logic. 1997. - Vol. 38, no. 1. — P. 1-18.

15. Chagrov A., Zakharyaschev M. Modal Logic. Oxford Logic Guides: vol. 35. — Clarendon Press, 1997.

16. Dashkov E. Arithmetical completeness of the intuitionistic logic of proofs // Journal of Logic and Computation. — 2011. — Vol. 21, no. 4. — P. 665-682.

17. Dunn J. Positive modal logic // Studia Logica. — 1995.— Vol. 55, no. 2.— P. 301-317.

18. Fitting M. The logic of proofs, semantically // Annals of Pure and Applied Logic. 2005. - Vol. 132, no. 1. - P. 1-25.

19. Ghilardi S. Unification in intuitionistic logic // The Journal of Symbolic Logic. 1999. - Vol. 64, no. 2. - P. 859-880.

20. Iemhoff R. On the admissible rules of intuitionistic propositional logic // The Journal of Symbolic Logic. 2001. - Vol. 66, no. 1. - P. 281-294.

21. Iemhoff R. Provability logic and admissible rules : PhD thesis / R. Iemhoff ; University of Amsterdam. — 2001.

22. Ignatiev K. On strong provability predicates and the associated modal logics // The Journal of Symbolic Logic. 1991. - Vol. 58, no. 1. - P. 249-290.

23. Kleene S. Introduction to Metamathematics. — D. van Nostrand Co., 1952.

24. Kripke S. Semantical analysis of intuitionistic logic I // Formal Systems and Recursive Functions / Ed. by J. Crossley, M. Dummett. — North-Holland Publishing Co., 1965.- P. 92-130.

25. Mkrtychev A. Models for the logic of proofs // Logical Foundations of Computer Science, 4th International Symposium LFCS'97 / Ed. by S.I. Adian, A. Nerode. — Lecture Notes in Computer Science 1234. — 1997. — P. 266-275.

26. Shapirovsky I. PSPACE-decidability of Japaridze's polymodal logic // Advarices in Modal Logic / Ed. by C. Areces, R. Goldblatt. — Vol. 7. — College Publications, 2008. P. 289-304.

27. Smorynski C. Applications of Kripke models // Mathematical Investigations of Intuitionistic Arithmetic and Analysis / Ed. by A. Troelstra. — Springer-Verlag, 1973. P. 324-391.

28. Smorynski C. Self-reference and modal logic. — Springer-Verlag, 1985.

29. Sofronie-Stokkermans V. Locality and subsumption testing in EL and some of its extensions // Advances in Modal Logic / Ed. by C. Areces, R. Goldblatt. — Vol. 7. College Publications, 2008. - P. 315-339.

30. Solovay R. Provability interpretation of modal logic // Israel Journal of Mathematics. 1976. - Vol. 25, no. 3-4. - P. 287-304.

31. Visser A. Aspects of diagonalization and provability : PhD. thesis / A. Visser ; Department of Philosophy, Utrecht University. — 1981.

32. Visser A. Rules and arithmetics // Notre Dame Journal of Formal Logic.— 1999.-Vol. 40, no. 1.- P. 116-140.