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

имени М. В. Ломоносова

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

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

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

понятие доказуемости

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

АВТОРЕФЕРАТ

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

Москва – 2012

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

Научный руководитель: Беклемишев Лев Дмитриевич член-корреспондент РАН

Официальные оппоненты: Артёмов Сергей Николаевич доктор физико-математических наук, профессор, The Graduate Center of the City University of New York, США, Distinguished Professor Шапировский Илья Борисович кандидат физико-математических наук, Институт проблем передачи информа­ ции имени А. А. Харкевича РАН, старший научный сотрудник

Ведущая организация: Институт математики имени С. Л. Соболева Сибирского отделения РАН

Защита состоится 28 сентября 2012 г. в 16 часов 45 минут на заседании диссер­ тационного совета Д 501.001.84 при Московском государственном университе­ те имени М. В. Ломоносова по адресу: РФ, 119991, Москва, ГСП-1, Ленинские горы, д. 1, МГУ, Механико-математический факультет, аудитория 14-08.

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

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

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

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

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

предполагают толкование есть доказательство. Логика LP полна от­ носительно арифметики Пеано PA при интерпретации : арифметической формулой * есть вывод * в арифметике Пеано.

Интуиционистская арифметика HA — наиболее известная теория, фор­ мализующая понятие конструктивного доказательства. В силу известных тео­ рем Р. Соловея,2 логикой доказуемости классической арифметики PA явля­ ется логика Гёделя–Лёба GL. Вопрос о логике доказуемости теории HA, впервые поставленный А. Виссером,3 длительное время остается открытым. Кроме того, — в частности, в связи с последним вопросом — представляет ин­ терес отыскание логики доказательств теории HA. Так, подходящим обра­ зом определенная интуиционистская логика доказательств позволяет выра­ Artemov S. Explicit provability and constructive semantics // The Bulletin for Symbolic Logic. — 2001. — Vol. 7, no. 1. — P. 1–36.

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

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

Beklemishev L., Visser A. Problems in the Logic of Provability // Mathematical Problems from Applied Log­ ic I: Logics for the XXIst Century / Ed. by D.M. Gabbay, S.S. Goncharov, M. Zakharyashev. — International Mathematical Series: vol. 4. Springer, 2006.

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

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

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

Кроме того, в настоящей диссертации предложена семантика Крипке для логик iBLP и iLP, развивающая подход А. Мкртычева8 и М. Фиттинга9 к Iemhoff R. Provability logic and admissible rules : PhD thesis / R. Iemhoff ; University of Amsterdam. — Artemov S. Unified semantics for modality and -terms via proof polynomials // Algebras, Diagrams and Decisions in Language, Logic and Computation / Ed. by K. Vermeulen, A. Copestake. — Stanford University, Artemov S., Iemhoff R. The basic intuitionistic logic of proofs // The Journal of Symbolic Logic. — 2007. — Vol. 72, no. 2. — P. 439–451.

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.

Fitting M. The logic of proofs, semantically // Annals of Pure and Applied Logic. — 2005. — Vol. 132, построению моделей логики доказательств. Доказаны соответствующие тео­ ремы о полноте и корректности, а также получен ряд следствий из них.

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

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

где [ ] означает класс эквивалентности формулы, а формула -Con ( ) естественным образом выражает совместность множества всех истинных -предложений и формулы в теории. Тогда градуированной алгеброй доказуемости теории называется структура = (, { | < }).

Термы можно отождествить с формулами некоторого модального языка.

Действительно, рассмотрим язык L с пропозициональными переменны­ ми, связками,,,, и для всех <. При этом считаем ¬, Для всякой (достаточно сильной) корректной теории логикой алгебры является система GLP, введенная Г. К. Джапаридзе11 в 1986 г. (см. тж.

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

Джапаридзе Г. К. Модально-логические средства исследования доказуемости : Дисс. канд. филос.

наук : 09.00.07 / Г. К. Джапаридзе ; МГУ. — M., 1986. — 177 с.

в изложении К. Н. Игнатьева12 ). Г. К. Джапаридзе фактически доказал, что для любой формулы языка L выполнено С применением логики GLP была получена система ординальных обо­ значений до ординала 0, ординальный анализ арифметики Пеано PA и ряда ее фрагментов,10 а также был построен новый пример комбинаторного утвер­ ждения, независимого от PA.13 В действительности, как заметил Л. Д. Бекле­ мишев, для получения этих результатов достаточно рассматривать позитив­ ный фрагмент GLP+ логики GLP, т. е. множество доказуемых в GLP эк­ вивалентностей формул позитивного * полимодального языка L+ с пропо­ зициональными переменными,, и модальными связками для всех <. Более того, упомянутая система ординальных обозначений строится из позитивных формул без переменных. Таким образом возможно упростить доказательства указанных результатов.

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

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

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

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

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

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.

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

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

Позитивные в некотором более широком смысле модальные логики рас­ сматривались ранее. Дж. Данн15 исследовал минимальную нормальную мо­ дальную логику K в языке LD со связками,,,,,, а также некото­ рые ее расширения. Аксиомами и теоремами при этом считаются утвержде­ ния вида. С помощью обычной семантики Крипке Данн установил, что K консервативна над K, или, другими словами, K аксиоматизирует фрагмент логики K в языке LD :

для любых, LD. Однако, в смысле предложенной семантики некото­ рые расширения K оказались неполными: например, в каждой шкале, где истинна утверждение не выводится из первого в K. Эта трудность была разрешена С. Челани и Р. Жансана,16 доказавшими полноту ряда расширений K отно­ сительно шкал, где отношение достижимости согласовано с некоторым пред­ порядком так, что допускаются лишь замкнутые вверх относительно предпо­ рядка оценки переменных.

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

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

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 позволяют получить аксиоматизацию пози­ тивных фрагментов многих хорошо известных логик, являющихся расши­ рениями K посредством принципов вида, где, LD. Таковы B, T, D, S4, S5 и др. Однако, например, к логике Гёделя–Лёба GL = K4 + ( ¬) эти результаты непосредственно не применимы. Из резуль­ татов настоящей работы следует совпадение L+ -фрагментов логик GL и K4, Вопросы сложности модальных логик в обедненных языках рассматрива­ лись ранее преимущественно в контексте дескрипционных логик. В дескрип­ ционной постановке исследовалась17,18,19,20 сложность задачи, представимой в модальных терминах следующим образом. Пусть формулы построены из переменных, связок,, и не более чем счетного множества связок.

Проверить: для всякой модели из данного класса, если во всех точках моде­ ли выполнено некоторое конечное множество импликаций, то во всех точках этой модели выполнена. Установлена ptime-разрешимость этой задачи для класса всех шкал Крипке и получены оценки сложности для некоторых классов шкал. Тем не менее, из известных нам результатов в этой области оценка сложности GLP+ очевидным образом не извлекается.

Целью диссертационной работы является следующее:

1. Доказать гипотезу Артёмова-Имхофф7 о полноте интуиционистской ло­ гики доказательств iLP относительно естественной арифметической се­ Baader F., Brandt S., Lutz C. Pushing the EL envelope // IJCAI / Ed. by L.P. Kaelbling, A. Saffiotti. — 2005. — P. 364–369.

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

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.

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.

мантики.

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

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

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

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

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

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

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

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

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

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

На международной конференции Advances in Modal Logic (Москва, На международном семинаре Proof, Computation, Complexity (Берн, Публикации. Основные результаты диссертации опубликованы в трех пе­ чатных работах автора [1–3], список которых приведен в конце автореферата.

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

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

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

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

Определение 1. Формулы и термы языка LiLP определяются индуктивно сле­ дующим образом. Пусть и суть формулы, а и термы. Тогда, p, :,,, суть формулы, где p пропозициональные переменные;

c, u, !, f, ·, + суть термы, где c и u доказательственные кон­ станты и переменные соответственно, а f для всех натуральных — специальные знаки операций над термами.

Определение 2. Для языка, содержащего булевы связки, и произвольного обозначим через Vn множество примеров схемы Определение 3. Логика доказательств iLP в языке LiLP определяется следу­ ющими схемами аксиом и правилами вывода:

A1 Схемы аксиом интуиционистской пропозициональной логики Определение 4. Будем рассматривать модели Крипке (,, ), где отно­ позициональных формул определим так, как для случая интуиционистской пропозициональной логики. Модель называется моделью Имхофф, если:

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

2. всякое конечное подмножество элементов модели имеет тесную ниж­ нюю грань, т. е. для каждого модель содержит такой элемент 0, что Определение 5. Пусть задана модель Имхофф KI и свидетельская функция E : TmLiLP 2LiLP, где TmLiLP обозначает множество термов LiLP, по опре­ делению удовлетворяющая условиям:

если — доказательственная константа, а — аксиома iLP, то Тогда KiLP = (KI, E) можно рассмотреть как модель языка LiLP :

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

Семантика для логики iLP получается комбинацией данной Имхофф семантической характеристики допустимых правил вывода интуиционистской пропозициональной логики с подходом Мкртычева8 и Фиттинга9 к построе­ нию моделей логики доказательств. Также используется техника проектив­ ных формул, развитая Гилярди. Определение 6. Предикат доказательств — это примитивно рекурсивная арифметическая формула Prf(, ), такая что при всех L0, где L означает множество арифметических предложений, HA имеет место тогда и только тогда, когда найдется число, для которого N |= Prf (, ).

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

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

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

причем функция { | ()} рекурсивная тотальная;

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

Тогда арифметическая интерпретация языка LiLP есть произвольное отоб­ ражение (·)* : LiLP TmLiLP L0, удовлетворяющее условиям:

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

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

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

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

Определение 8. Полимодальный пропозициональный язык L имеет связки,,,, и для всех. Позитивный язык L+ получается из L исключением всех связок, кроме, и для всех. Позитивный мономодальный язык L+ (0) имеет связки, и, причем последнюю мы отождествляем с 0 и считаем L+ (0) L+.

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

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

(ii) ¬;

(vii), если <, и правилами вывода: modus ponens и (Nec).

Определение 10. Множество формальных равенств GLP+ GLP и, L+ } называется позитивным фрагментом логи­ ки GLP. Задаваемое GLP+ отношение = на (L+ )2 действительно является отношением эквивалентности.

Определение 11. Определим исчисление GLPe для равенств вида =, где, L+. Примем схему аксиом = и правила для всех <. Пусть правил, исчисление GLPe задается схемами аксиом Теорема 3. Пусть, L+. Тогда GLP равносильно GLPe Определение 12. Шкала Крипке (, { } ) называется + -шкалой, если Вынуждение формул языка L определяется обычным образом.

когда в каждой (конечной) + -модели вынуждается.

Определение 13. Исчисление K4e в языке L+ (0) получается, если в опреде­ лении GLPe ограничиться аксиомой и правилами для =, а также неравен­ ствами (1–6), полагая всюду в последних = 0.

Теорема 5. Пусть L есть произвольная мономодальная логика, промежу­ точная между K4 и GL. Тогда L равносильно K4e = для всех, L+ (0).

Определение 14. Сложность || формулы L+ есть ее длина как слова в Теорема 6. Проблема принадлежности к множеству GLP+ равенств вида = разрешима за время, полиномиальное от = || + ||.

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

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

Beklemishev L. Kripke 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.