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

• Дашков, Евгений Владимирович
• кандидат физико-математических наук
• 2012

Оглавление диссертации кандидат физико-математических наук Дашков, Евгений Владимирович

Введение.

Глава 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].

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Дашков, Евгений Владимирович, 2012 год

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.